Mmsolitaire
My contributions to Metamath's mmsolitaire project.
Install / Use
/learn @xamidi/MmsolitaireREADME
@xamidi/mmsolitaire (repository)
Branch of metamath/mmsolitaire/pmproofs of the Metamath Solitaire project.
Contributions
- [2be2349] found 17 shorter proofs (proposal)
- [21911f8] found 5 shorter proofs (proposal)
- [f9a40e7] found 40 shorter proofs (proposal)
- [9bb17b0] found 38 shorter proofs (proposal)
Summary
| | Formula | Improvement(s) | Reduced by |
| -- | -- | -- | --:|
| *2.32 | <a name="((ψ∨φ)∨χ)→(ψ∨(φ∨χ))" href="#((ψ∨φ)∨χ)→(ψ∨(φ∨χ))" title="((ψ∨φ)∨χ)→(ψ∨(φ∨χ))">CAApqrApAqr</a> | 91↦83 | 8 |
| *2.62 | <a name="(ψ∨φ)→((ψ→φ)→φ)" href="#(ψ∨φ)→((ψ→φ)→φ)" title="(ψ∨φ)→((ψ→φ)→φ)">CApqCCpqq</a> | 89↦77 | 12 |
| *2.73 | <a name="(ψ→φ)→(((ψ∨φ)∨χ)→(φ∨χ))" href="#(ψ→φ)→(((ψ∨φ)∨χ)→(φ∨χ))" title="(ψ→φ)→(((ψ∨φ)∨χ)→(φ∨χ))">CCpqCAApqrAqr</a> | 165↦153 | 12 |
| *2.82 | <a name="((ψ∨φ)∨χ)→(((ψ∨¬χ)∨ξ)→((ψ∨φ)∨ξ))" href="#((ψ∨φ)∨χ)→(((ψ∨¬χ)∨ξ)→((ψ∨φ)∨ξ))" title="((ψ∨φ)∨χ)→(((ψ∨¬χ)∨ξ)→((ψ∨φ)∨ξ))">CAApqrCAApNrsAApqs</a> | 91↦89 | 2 |
| *3.3 Exp | <a name="((ψ∧φ)→χ)→(ψ→(φ→χ))" href="#((ψ∧φ)→χ)→(ψ→(φ→χ))" title="((ψ∧φ)→χ)→(ψ→(φ→χ))">CCKpqrCpCqr</a> | 59↦55 | 4 |
| *3.31 Imp | <a name="(ψ→(φ→χ))→((ψ∧φ)→χ)" href="#(ψ→(φ→χ))→((ψ∧φ)→χ)" title="(ψ→(φ→χ))→((ψ∧φ)→χ)">CCpCqrCKpqr</a> | 103↦83 | 20 |
| *3.33 Syll | <a name="((ψ→φ)∧(φ→χ))→(ψ→χ)" href="#((ψ→φ)∧(φ→χ))→(ψ→χ)" title="((ψ→φ)∧(φ→χ))→(ψ→χ)">CKCpqCqrCpr</a> | 95↦73 | 22 |
| *3.34 Syll | <a name="((φ→χ)∧(ψ→φ))→(ψ→χ)" href="#((φ→χ)∧(ψ→φ))→(ψ→χ)" title="((φ→χ)∧(ψ→φ))→(ψ→χ)">CKCpqCrpCrq</a> | 105↦73 | 32 |
| *3.43 Comp | <a name="((ψ→φ)∧(ψ→χ))→(ψ→(φ∧χ))" href="#((ψ→φ)∧(ψ→χ))→(ψ→(φ∧χ))" title="((ψ→φ)∧(ψ→χ))→(ψ→(φ∧χ))">CKCpqCprCpKqr</a> | 137↦109 | 28 |
| *3.44 | <a name="((φ→ψ)∧(χ→ψ))→((φ∨χ)→ψ)" href="#((φ→ψ)∧(χ→ψ))→((φ∨χ)→ψ)" title="((φ→ψ)∧(χ→ψ))→((φ∨χ)→ψ)">CKCpqCrqCAprq</a> | 203↦161 | 42 |
| *3.47 | <a name="((ψ→χ)∧(φ→ξ))→((ψ∧φ)→(χ∧ξ))" href="#((ψ→χ)∧(φ→ξ))→((ψ∧φ)→(χ∧ξ))" title="((ψ→χ)∧(φ→ξ))→((ψ∧φ)→(χ∧ξ))">CKCpqCrsCKprKqs</a> | 203↦199 | 4 |
| *3.48 | <a name="((ψ→χ)∧(φ→ξ))→((ψ∨φ)→(χ∨ξ))" href="#((ψ→χ)∧(φ→ξ))→((ψ∨φ)→(χ∨ξ))" title="((ψ→χ)∧(φ→ξ))→((ψ∨φ)→(χ∨ξ))">CKCpqCrsCAprAqs</a> | 241↦167 | 74 |
| *4.11 | <a name="(ψ↔φ)↔(¬ψ↔¬φ)" href="#(ψ↔φ)↔(¬ψ↔¬φ)" title="(ψ↔φ)↔(¬ψ↔¬φ)">EEpqENpNq</a> | 363↦359 | 4 |
| *4.12 | <a name="(ψ↔¬φ)↔(φ↔¬ψ)" href="#(ψ↔¬φ)↔(φ↔¬ψ)" title="(ψ↔¬φ)↔(φ↔¬ψ)">EEpNqEqNp</a> | 363↦359 | 4 |
| *4.14 | <a name="((ψ∧φ)→χ)↔((ψ∧¬χ)→¬φ)" href="#((ψ∧φ)→χ)↔((ψ∧¬χ)→¬φ)" title="((ψ∧φ)→χ)↔((ψ∧¬χ)→¬φ)">ECKpqrCKpNrNq</a> | 321↦263 | 58 |
| *4.15 | <a name="((ψ∧φ)→¬χ)↔((φ∧χ)→¬ψ)" href="#((ψ∧φ)→¬χ)↔((φ∧χ)→¬ψ)" title="((ψ∧φ)→¬χ)↔((φ∧χ)→¬ψ)">ECKpqNrCKqrNp</a> | 277↦205 | 72 |
| *4.22 | <a name="((ψ↔φ)∧(φ↔χ))→(ψ↔χ)" href="#((ψ↔φ)∧(φ↔χ))→(ψ↔χ)" title="((ψ↔φ)∧(φ↔χ))→(ψ↔χ)">CKEpqEqrEpr</a> | 273↦271 | 2 |
| *4.32 | <a name="((ψ∧φ)∧χ)↔(ψ∧(φ∧χ))" href="#((ψ∧φ)∧χ)↔(ψ∧(φ∧χ))" title="((ψ∧φ)∧χ)↔(ψ∧(φ∧χ))">EKKpqrKpKqr</a> | 355↦313 | 42 |
| *4.33 | <a name="((ψ∨φ)∨χ)↔(ψ∨(φ∨χ))" href="#((ψ∨φ)∨χ)↔(ψ∨(φ∨χ))" title="((ψ∨φ)∨χ)↔(ψ∨(φ∨χ))">EAApqrApAqr</a> | 207↦199 | 8 |
| *4.36 | <a name="(ψ↔φ)→((ψ∧χ)↔(φ∧χ))" href="#(ψ↔φ)→((ψ∧χ)↔(φ∧χ))" title="(ψ↔φ)→((ψ∧χ)↔(φ∧χ))">CEpqEKprKqr</a> | 271↦219 | 52 |
| *4.37 | <a name="(ψ↔φ)→((ψ∨χ)↔(φ∨χ))" href="#(ψ↔φ)→((ψ∨χ)↔(φ∨χ))" title="(ψ↔φ)→((ψ∨χ)↔(φ∨χ))">CEpqEAprAqr</a> | 307↦255 | 52 |
| *4.38 | <a name="((ψ↔χ)∧(φ↔ξ))→((ψ∧φ)↔(χ∧ξ))" href="#((ψ↔χ)∧(φ↔ξ))→((ψ∧φ)↔(χ∧ξ))" title="((ψ↔χ)∧(φ↔ξ))→((ψ∧φ)↔(χ∧ξ))">CKEpqErsEKprKqs</a> | 585↦527 | 58 |
| *4.39 | <a name="((ψ↔χ)∧(φ↔ξ))→((ψ∨φ)↔(χ∨ξ))" href="#((ψ↔χ)∧(φ↔ξ))→((ψ∨φ)↔(χ∨ξ))" title="((ψ↔χ)∧(φ↔ξ))→((ψ∨φ)↔(χ∨ξ))">CKEpqErsEAprAqs</a> | 609↦463 | 146 |
| *4.4 | <a name="(ψ∧(φ∨χ))↔((ψ∧φ)∨(ψ∧χ))" href="#(ψ∧(φ∨χ))↔((ψ∧φ)∨(ψ∧χ))" title="(ψ∧(φ∨χ))↔((ψ∧φ)∨(ψ∧χ))">EKpAqrAKpqKpr</a> | 355↦345 | 10 |
| *4.41 | <a name="(ψ∨(φ∧χ))↔((ψ∨φ)∧(ψ∨χ))" href="#(ψ∨(φ∧χ))↔((ψ∨φ)∧(ψ∨χ))" title="(ψ∨(φ∧χ))↔((ψ∨φ)∧(ψ∨χ))">EApKqrKApqApr</a> | 271↦241 | 30 |
| *4.42 | <a name="ψ↔((ψ∧φ)∨(ψ∧¬φ))" href="#ψ↔((ψ∧φ)∨(ψ∧¬φ))" title="ψ↔((ψ∧φ)∨(ψ∧¬φ))">EpAKpqKpNq</a> | 165↦157 | 8 |
| *4.52 | <a name="(ψ∧¬φ)↔¬(¬ψ∨φ)" href="#(ψ∧¬φ)↔¬(¬ψ∨φ)" title="(ψ∧¬φ)↔¬(¬ψ∨φ)">EKpNqNANpq</a> | 219↦207 | 12 |
| *4.53 | <a name="¬(ψ∧¬φ)↔(¬ψ∨φ)" href="#¬(ψ∧¬φ)↔(¬ψ∨φ)" title="¬(ψ∧¬φ)↔(¬ψ∨φ)">ENKpNqANpq</a> | 169↦157 | 12 |
| *4.72 | <a name="(ψ→φ)↔(φ↔(ψ∨φ))" href="#(ψ→φ)↔(φ↔(ψ∨φ))" title="(ψ→φ)↔(φ↔(ψ∨φ))">ECpqEqApq</a> | 195↦193 | 2 |
| *4.76 | <a name="((ψ→φ)∧(ψ→χ))↔(ψ→(φ∧χ))" href="#((ψ→φ)∧(ψ→χ))↔(ψ→(φ∧χ))" title="((ψ→φ)∧(ψ→χ))↔(ψ→(φ∧χ))">EKCpqCprCpKqr</a> | 271↦241 | 30 |
| *4.77 | <a name="((φ→ψ)∧(χ→ψ))↔((φ∨χ)→ψ)" href="#((φ→ψ)∧(χ→ψ))↔((φ∨χ)→ψ)" title="((φ→ψ)∧(χ→ψ))↔((φ∨χ)→ψ)">EKCpqCrqCAprq</a> | 375↦265 | 110 |
| *4.78 | <a name="((ψ→φ)∨(ψ→χ))↔(ψ→(φ∨χ))" href="#((ψ→φ)∨(ψ→χ))↔(ψ→(φ∨χ))" title="((ψ→φ)∨(ψ→χ))↔(ψ→(φ∨χ))">EACpqCprCpAqr</a> | 319↦191 | 128 |
| *4.79 | <a name="((φ→ψ)∨(χ→ψ))↔((φ∧χ)→ψ)" href="#((φ→ψ)∨(χ→ψ))↔((φ∧χ)→ψ)" title="((φ→ψ)∨(χ→ψ))↔((φ∧χ)→ψ)">EACpqCrqCKprq</a> | 383↦259 | 124 |
| *4.82 | <a name="((ψ→φ)∧(ψ→¬φ))↔¬ψ" href="#((ψ→φ)∧(ψ→¬φ))↔¬ψ" title="((ψ→φ)∧(ψ→¬φ))↔¬ψ">EKCpqCpNqNp</a> | 175↦157 | 18 |
| *4.83 | <a name="((ψ→φ)∧(¬ψ→φ))↔φ" href="#((ψ→φ)∧(¬ψ→φ))↔φ" title="((ψ→φ)∧(¬ψ→φ))↔φ">EKCpqCNpqq</a> | 245↦197 | 48 |
| *4.85 | <a name="(ψ↔φ)→((χ→ψ)↔(χ→φ))" href="#(ψ↔φ)→((χ→ψ)↔(χ→φ))" title="(ψ↔φ)→((χ→ψ)↔(χ→φ))">CEpqECrpCrq</a> | 123↦119 | 4 |
| *4.86 | <a name="(ψ↔φ)→((ψ↔χ)↔(φ↔χ))" href="#(ψ↔φ)→((ψ↔χ)↔(φ↔χ))" title="(ψ↔φ)→((ψ↔χ)↔(φ↔χ))">CEpqEEprEqr</a> | 617↦473 | 144 |
| *4.87 | <a name="((((ψ∧φ)→χ)↔(ψ→(φ→χ)))∧((ψ→(φ→χ))↔(φ→(ψ→χ))))∧((φ→(ψ→χ))↔((φ∧ψ)→χ))" href="#((((ψ∧φ)→χ)↔(ψ→(φ→χ)))∧((ψ→(φ→χ))↔(φ→(ψ→χ))))∧((φ→(ψ→χ))↔((φ∧ψ)→χ))" title="((((ψ∧φ)→χ)↔(ψ→(φ→χ)))∧((ψ→(φ→χ))↔(φ→(ψ→χ))))∧((φ→(ψ→χ))↔((φ∧ψ)→χ))">KKECKpqrCpCqrECpCqrCqCprECqCprCKqpr</a> | 523↦439 | 84 |
| *5.1 | <a name="(ψ∧φ)→(ψ↔φ)" href="#(ψ∧φ)→(ψ↔φ)" title="(ψ∧φ)→(ψ↔φ)">CKpqEpq</a> | 107↦87 | 20 |
| *5.15 | <a name="(ψ↔φ)∨(ψ↔¬φ)" href="#(ψ↔φ)∨(ψ↔¬φ)" title="(ψ↔φ)∨(ψ↔¬φ)">AEpqEpNq</a> | 267↦161 | 106 |
| *5.16 | <a name="¬((ψ↔φ)∧(ψ↔¬φ))" href="#¬((ψ↔φ)∧(ψ↔¬φ))" title="¬((ψ↔φ)∧(ψ↔¬φ))">NKEpqEpNq</a> | 333↦331 | 2 |
| *5.17 | <a name="((ψ∨φ)∧¬(ψ∧φ))↔(ψ↔¬φ)" href="#((ψ∨φ)∧¬(ψ∧φ))↔(ψ↔¬φ)" title="((ψ∨φ)∧¬(ψ∧φ))↔(ψ↔¬φ)">EKApqNKpqEpNq</a> | 329↦285 | 44 |
| *5.18 | <a name="(ψ↔φ)↔¬(ψ↔¬φ)" href="#(ψ↔φ)↔¬(ψ↔¬φ)" title="(ψ↔φ)↔¬(ψ↔¬φ)">EEpqNEpNq</a> | 503↦491 | 12 |
| *5.19 | <a name="¬(ψ↔¬ψ)" href="#¬(ψ↔¬ψ)" title="¬(ψ↔¬ψ)">NEpNp</a> | 123↦105 | 18 |
| *5.21 | <a name="(¬ψ∧¬φ)→(ψ↔φ)" href="#(¬ψ∧¬φ)→(ψ↔φ)" title="(¬ψ∧¬φ)→(ψ↔φ)">CKNpNqEpq</a> | 115↦111 | 4 |
| *5.22 | <a name="¬(ψ↔φ)↔((ψ∧¬φ)∨(φ∧¬ψ))" href="#¬(ψ↔φ)↔((ψ∧¬φ)∨(φ∧¬ψ))" title="¬(ψ↔φ)↔((ψ∧¬φ)∨(φ∧¬ψ))">ENEpqAKpNqKqNp</a> | 363↦333 | 30 |
| *5.23 | <a name="(ψ↔φ)↔((ψ∧φ)∨(¬ψ∧¬φ))" href="#(ψ↔φ)↔((ψ∧φ)∨(¬ψ∧¬φ))" title="(ψ↔φ)↔((ψ∧φ)∨(¬ψ∧¬φ))">EEpqAKpqKNpNq</a> | 513↦501 | 12 |
| *5.24 | <a name="¬((ψ∧φ)∨(¬ψ∧¬φ))↔((ψ∧¬φ)∨(φ∧¬ψ))" href="#¬((ψ∧φ)∨(¬ψ∧¬φ))↔((ψ∧¬φ)∨(φ∧¬ψ))" title="¬((ψ∧φ)∨(¬ψ∧¬φ))↔((ψ∧¬φ)∨(φ∧¬ψ))">ENAKpqKNpNqAKpNqKqNp</a> | 585↦545 | 40 |
| *5.3 | <a name="((ψ∧φ)→χ)↔((ψ∧φ)→(ψ∧χ))" href="#((ψ∧φ)→χ)↔((ψ∧φ)→(ψ∧χ))" title="((ψ∧φ)→χ)↔((ψ∧φ)→(ψ∧χ))">ECKpqrCKpqKpr</a> | 127↦125 | 2 |
| *5.31 | <a name="(χ∧(ψ→φ))→(ψ→(φ∧χ))" href="#(χ∧(ψ→φ))→(ψ→(φ∧χ))" title="(χ∧(ψ→φ))→(ψ→(φ∧χ))">CKpCqrCqKrp</a> | 119↦105 | 14 |
| *5.32 | <a name="(ψ→(φ↔χ))↔((ψ∧φ)↔(ψ∧χ))" href="#(ψ→(φ↔χ))↔((ψ∧φ)↔(ψ∧χ))" title="(ψ→(φ↔χ))↔((ψ∧φ)↔(ψ∧χ))">ECpEqrEKpqKpr</a> | 625↦621 | 4 |
| *5.33 | <a name="(ψ∧(φ→χ))↔(ψ∧((ψ∧φ)→χ))" href="#(ψ∧(φ→χ))↔(ψ∧((ψ∧φ)→χ))" title="(ψ∧(φ→χ))↔(ψ∧((ψ∧φ)→χ))">EKpCqrKpCKpqr</a> | 389↦311 | 78 |
| *5.35 | <a name="((ψ→φ)∧(ψ→χ))→(ψ→(φ↔χ))" href="#((ψ→φ)∧(ψ→χ))→(ψ→(φ↔χ))" title="((ψ→φ)∧(ψ→χ))→(ψ→(φ↔χ))">CKCpqCprCpEqr</a> | 159↦129 | 30 |
| *5.36 | <a name="(ψ∧(ψ↔φ))↔(φ∧(ψ↔φ))" href="#(ψ∧(ψ↔φ))↔(φ∧(ψ↔φ))" title="(ψ∧(ψ↔φ))↔(φ∧(ψ↔φ))">EKpEpqKqEpq</a> | 381↦257 | 124 |
| *5.53 | <a name="(((ψ∨φ)∨χ)→ξ)↔(((ψ→ξ)∧(φ→ξ))∧(χ→ξ))" href="#(((ψ∨φ)∨χ)→ξ)↔(((ψ→ξ)∧(φ→ξ))∧(χ→ξ))" title="(((ψ∨φ)∨χ)→ξ)↔(((ψ→ξ)∧(φ→ξ))∧(χ→ξ))">ECAApqrsKKCpsCqsCrs</a> | 673↦551 | 122 |
| *5.54 | <a name="((ψ∧φ)↔ψ)∨((ψ∧φ)↔φ)" href="#((ψ∧φ)↔ψ)∨((ψ∧φ)↔φ)" title="((ψ∧φ)↔ψ)∨((ψ∧φ)↔φ)">AEKpqpEKpqq</a> | 239↦149 | 90 |
| *5.55 | <a name="((ψ∨φ)↔ψ)∨((ψ∨φ)↔φ)" href="#((ψ∨φ)↔ψ)∨((ψ∨φ)↔φ)" title="((ψ∨φ)↔ψ)∨((ψ∨φ)↔φ)">AEApqpEApqq</a> | 167↦165 | 2 |
| *5.6 | <a name="((ψ∧¬φ)→χ)↔(ψ→(φ∨χ))" href="#((ψ∧¬φ)→χ)↔(ψ→(φ∨χ))" title="((ψ∧¬φ)→χ)↔(ψ→(φ∨χ))">ECKpNqrCpAqr</a> | 203↦163 | 40 |
| *5.61 | <a name="((ψ∨φ)∧¬φ)↔(ψ∧¬φ)" href="#((ψ∨φ)∧¬φ)↔(ψ∧¬φ)" title="((ψ∨φ)∧¬φ)↔(ψ∧¬φ)">EKApqNqKpNq</a> | 259↦231 | 28 |
| *5.62 | <a name="((ψ∧φ)∨¬φ)↔(ψ∨¬φ)" href="#((ψ∧φ)∨¬φ)↔(ψ∨¬φ)" title="((ψ∧φ)∨¬φ)↔(ψ∨¬φ)">EAKpqNqApNq</a> | 167↦157 | 10 |
| *5.7 | <a name="((ψ∨χ)↔(φ∨χ))↔(χ∨(ψ↔φ))" href="#((ψ∨χ)↔(φ∨χ))↔(χ∨(ψ↔φ))" title="((ψ∨χ)↔(φ∨χ))↔(χ∨(ψ↔φ))">EEApqArqAqEpr</a> | 673↦605 | 68 |
| *5.74 | <a name="(ψ→(φ↔χ))↔((ψ→φ)↔(ψ→χ))" href="#(ψ→(φ↔χ))↔((ψ→φ)↔(ψ→χ))" title="(ψ→(φ↔χ))↔((ψ→φ)↔(ψ→χ))">ECpEqrECpqCpr</a> | 337↦333 | 4 |
| *5.75 | <a name="((χ→¬φ)∧(ψ↔(φ∨χ)))→((ψ∧¬φ)↔χ)" href="#((χ→¬φ)∧(ψ↔(φ∨χ)))→((ψ∧¬φ)↔χ)" title="((χ→¬φ)∧(ψ↔(φ∨χ)))→((ψ∧¬φ)↔χ)">CKCpNqErAqpEKrNqp</a> | 387↦331 | 56 |
| meredith | <a name="((((ψ→φ)→(¬χ→¬ξ))→χ)→τ)→((τ→ψ)→(ξ→ψ))" href="#((((ψ→φ)→(¬χ→¬ξ))→χ)→
Security Score
Audited on Mar 31, 2025