Metamath Proof Explorer

Theorem adh-minim-ax1

Description: Derivation of ax-1 from adh-minim and ax-mp . Carew Arthur Meredith derived ax-1 inA 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.)

Ref Expression
Assertion adh-minim-ax1 ⊢ φ → ψ → φ

Proof

Step Hyp Ref Expression
1 adh-minim-ax1-ax2-lem1 ⊢ φ → ψ → χ → θ → ψ → τ → θ → τ → φ → ψ → φ
2 adh-minim-ax1-ax2-lem1 ⊢ ψ → φ → ψ → η → ζ → ψ → σ → ζ → σ → χ → θ → ψ → τ → θ → τ → φ → ψ → χ → θ → ψ → τ → θ → τ → φ
3 adh-minim-ax1-ax2-lem3 ⊢ χ → θ → ψ → τ → θ → τ → ψ → φ → ψ → η → ζ → ψ → σ → ζ → σ → χ → θ → ψ → τ → θ → τ → φ
4 adh-minim-ax1-ax2-lem4 ⊢ χ → θ → ψ → τ → θ → τ → ψ → φ → ψ → η → ζ → ψ → σ → ζ → σ → χ → θ → ψ → τ → θ → τ → φ → ψ → φ → ψ → η → ζ → ψ → σ → ζ → σ → χ → θ → ψ → τ → θ → τ → φ → ψ → χ → θ → ψ → τ → θ → τ → φ → ψ → φ → ψ → χ → θ → ψ → τ → θ → τ → φ
5 3 4 ax-mp ⊢ ψ → φ → ψ → η → ζ → ψ → σ → ζ → σ → χ → θ → ψ → τ → θ → τ → φ → ψ → χ → θ → ψ → τ → θ → τ → φ → ψ → φ → ψ → χ → θ → ψ → τ → θ → τ → φ
6 2 5 ax-mp ⊢ ψ → φ → ψ → χ → θ → ψ → τ → θ → τ → φ
7 adh-minim-ax1-ax2-lem4 ⊢ ψ → φ → ψ → χ → θ → ψ → τ → θ → τ → φ → φ → ψ → χ → θ → ψ → τ → θ → τ → φ → ψ → φ → φ → ψ → φ
8 6 7 ax-mp ⊢ φ → ψ → χ → θ → ψ → τ → θ → τ → φ → ψ → φ → φ → ψ → φ
9 1 8 ax-mp ⊢ φ → ψ → φ