Theorem adh-minim-ax1 47784

Description: Derivation of ax-1 6 from adh-minim 47779 and ax-mp 5. Carew Arthur Meredith derived ax-1 6 in A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170. However, here we follow the shortened derivation by Ivo Thomas, On Meredith's sole positive axiom, Notre Dame Journal of Formal Logic, volume XV, number 3, July 1974, page 477. Polish prefix notation: CpCqp . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
adh-minim-ax1	⊢ (𝜑 → (𝜓 → 𝜑))

Proof of Theorem adh-minim-ax1

Step	Hyp	Ref	Expression
1		adh-minim-ax1-ax2-lem1 47780	. 2 ⊢ (𝜑 → ((𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑)) → (𝜓 → 𝜑)))
2		adh-minim-ax1-ax2-lem1 47780	. . . 4 ⊢ ((𝜓 → 𝜑) → ((𝜓 → ((𝜂 → ((𝜁 → (𝜓 → 𝜎)) → (𝜁 → 𝜎))) → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑))) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑))))
3		adh-minim-ax1-ax2-lem3 47782	. . . . 5 ⊢ (((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → (𝜓 → 𝜑)) → (𝜓 → ((𝜂 → ((𝜁 → (𝜓 → 𝜎)) → (𝜁 → 𝜎))) → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑))))
4		adh-minim-ax1-ax2-lem4 47783	. . . . 5 ⊢ ((((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → (𝜓 → 𝜑)) → (𝜓 → ((𝜂 → ((𝜁 → (𝜓 → 𝜎)) → (𝜁 → 𝜎))) → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑)))) → (((𝜓 → 𝜑) → ((𝜓 → ((𝜂 → ((𝜁 → (𝜓 → 𝜎)) → (𝜁 → 𝜎))) → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑))) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑)))) → ((𝜓 → 𝜑) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑)))))
5	3, 4	ax-mp 5	. . . 4 ⊢ (((𝜓 → 𝜑) → ((𝜓 → ((𝜂 → ((𝜁 → (𝜓 → 𝜎)) → (𝜁 → 𝜎))) → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑))) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑)))) → ((𝜓 → 𝜑) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑))))
6	2, 5	ax-mp 5	. . 3 ⊢ ((𝜓 → 𝜑) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑)))
7		adh-minim-ax1-ax2-lem4 47783	. . 3 ⊢ (((𝜓 → 𝜑) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑))) → ((𝜑 → ((𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑)) → (𝜓 → 𝜑))) → (𝜑 → (𝜓 → 𝜑))))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝜑 → ((𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜑)) → (𝜓 → 𝜑))) → (𝜑 → (𝜓 → 𝜑)))
9	1, 8	ax-mp 5	1 ⊢ (𝜑 → (𝜓 → 𝜑))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  adh-minim-ax2-lem5  47785  adh-minim-idALT  47789  adh-minim-pm2.43  47790