Theorem adh-minim 43311

Description: A 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. This is the axiom from Carew Arthur Meredith, A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170. A two-line review by Alonzo Church of this article can be found in The Journal of Symbolic Logic, volume 19, issue 2, June 1954, page 144, https://doi.org/10.2307/2268914. Known as "HI-1" on Dolph Edward "Ted" Ulrich's web page. In the next 6 lemmas and 3 theorems, ax-1 6 and ax-2 7 are derived from this single axiom in 16 detachments (instances of ax-mp 5) in total. Polish prefix notation: CCCpqrCsCCqCrtCqt . (Contributed by ADH, 10-Nov-2023.)

Assertion

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

Proof of Theorem adh-minim

Step	Hyp	Ref	Expression
1		pm2.04 90	. . . . 5 ⊢ ((𝜓 → (𝜒 → 𝜏)) → (𝜒 → (𝜓 → 𝜏)))
2		adh-jarrsc 43310	. . . . . . . 8 ⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜒)))
3		pm2.04 90	. . . . . . . . . . 11 ⊢ ((𝜒 → (𝜓 → 𝜏)) → (𝜓 → (𝜒 → 𝜏)))
4		ax-2 7	. . . . . . . . . . . 12 ⊢ ((𝜓 → (𝜒 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏)))
5		imim2 58	. . . . . . . . . . . 12 ⊢ (((𝜓 → (𝜒 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏))) → (((𝜒 → (𝜓 → 𝜏)) → (𝜓 → (𝜒 → 𝜏))) → ((𝜒 → (𝜓 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏)))))
6	4, 5	ax-mp 5	. . . . . . . . . . 11 ⊢ (((𝜒 → (𝜓 → 𝜏)) → (𝜓 → (𝜒 → 𝜏))) → ((𝜒 → (𝜓 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏))))
7	3, 6	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝜒 → (𝜓 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏)))
8		ax-2 7	. . . . . . . . . 10 ⊢ (((𝜒 → (𝜓 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏))) → (((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜒)) → ((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜏))))
9	7, 8	ax-mp 5	. . . . . . . . 9 ⊢ (((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜒)) → ((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜏)))
10		imim2 58	. . . . . . . . 9 ⊢ ((((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜒)) → ((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜏))) → ((((𝜑 → 𝜓) → 𝜒) → ((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜒))) → (((𝜑 → 𝜓) → 𝜒) → ((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜏)))))
11	9, 10	ax-mp 5	. . . . . . . 8 ⊢ ((((𝜑 → 𝜓) → 𝜒) → ((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜒))) → (((𝜑 → 𝜓) → 𝜒) → ((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜏))))
12	2, 11	ax-mp 5	. . . . . . 7 ⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜏)))
13		pm2.04 90	. . . . . . 7 ⊢ ((((𝜑 → 𝜓) → 𝜒) → ((𝜒 → (𝜓 → 𝜏)) → (𝜓 → 𝜏))) → ((𝜒 → (𝜓 → 𝜏)) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜏))))
14	12, 13	ax-mp 5	. . . . . 6 ⊢ ((𝜒 → (𝜓 → 𝜏)) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜏)))
15		imim2 58	. . . . . 6 ⊢ (((𝜒 → (𝜓 → 𝜏)) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜏))) → (((𝜓 → (𝜒 → 𝜏)) → (𝜒 → (𝜓 → 𝜏))) → ((𝜓 → (𝜒 → 𝜏)) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜏)))))
16	14, 15	ax-mp 5	. . . . 5 ⊢ (((𝜓 → (𝜒 → 𝜏)) → (𝜒 → (𝜓 → 𝜏))) → ((𝜓 → (𝜒 → 𝜏)) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜏))))
17	1, 16	ax-mp 5	. . . 4 ⊢ ((𝜓 → (𝜒 → 𝜏)) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜏)))
18		pm2.04 90	. . . 4 ⊢ (((𝜓 → (𝜒 → 𝜏)) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜏))) → (((𝜑 → 𝜓) → 𝜒) → ((𝜓 → (𝜒 → 𝜏)) → (𝜓 → 𝜏))))
19	17, 18	ax-mp 5	. . 3 ⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜓 → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))
20		ax-1 6	. . 3 ⊢ ((((𝜑 → 𝜓) → 𝜒) → ((𝜓 → (𝜒 → 𝜏)) → (𝜓 → 𝜏))) → (𝜃 → (((𝜑 → 𝜓) → 𝜒) → ((𝜓 → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))))
21	19, 20	ax-mp 5	. 2 ⊢ (𝜃 → (((𝜑 → 𝜓) → 𝜒) → ((𝜓 → (𝜒 → 𝜏)) → (𝜓 → 𝜏))))
22		pm2.04 90	. 2 ⊢ ((𝜃 → (((𝜑 → 𝜓) → 𝜒) → ((𝜓 → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))) → (((𝜑 → 𝜓) → 𝜒) → (𝜃 → ((𝜓 → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))))
23	21, 22	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-minim-ax1-ax2-lem1  43312  adh-minim-ax1-ax2-lem4  43315