Theorem adh-minimp 43323

Description: Another single axiom for minimal implicational calculus, due to Meredith. Other single axioms of the same length are known, but it is thought to be the minimal length. Among single axioms of this length, it is the one with simplest antecedents (i.e., in the corresponding ordering of binary trees which first compares left subtrees, it is the first one). Known as "HI-2" on Dolph Edward "Ted" Ulrich's web page. In the next 4 lemmas and 5 theorems, ax-1 6 and ax-2 7 are derived from this other single axiom in 20 detachments (instances of ax-mp 5) in total. Polish prefix notation: CpCCqrCCCsqCrtCqt ; or CtCCpqCCCspCqrCpr in Carew Arthur Meredith and Arthur Norman Prior, Notes on the axiomatics of the propositional calculus, Notre Dame Journal of Formal Logic, volume IV, number 3, July 1963, pages 171--187, on page 180. (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.)

Assertion

Ref	Expression
adh-minimp	⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏))))

Proof of Theorem adh-minimp

Step	Hyp	Ref	Expression
1		jarr 106	. . . 4 ⊢ (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → (𝜒 → 𝜏)))
2		ax-2 7	. . . . 5 ⊢ ((𝜓 → (𝜒 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏)))
3		imim2 58	. . . . 5 ⊢ (((𝜓 → (𝜒 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏))) → ((((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → (𝜒 → 𝜏))) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏)))))
4	2, 3	ax-mp 5	. . . 4 ⊢ ((((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → (𝜒 → 𝜏))) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏))))
5	1, 4	ax-mp 5	. . 3 ⊢ (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏)))
6		pm2.04 90	. . 3 ⊢ ((((𝜃 → 𝜓) → (𝜒 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏))) → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏))))
7	5, 6	ax-mp 5	. 2 ⊢ ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))
8		ax-1 6	. 2 ⊢ (((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏))) → (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))))
9	7, 8	ax-mp 5	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏))))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  adh-minimp-jarr-imim1-ax2c-lem1  43324  adh-minimp-jarr-lem2  43325