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	$⊢ φ \to (ψ \to φ)$

Proof

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

Metamath Proof Explorer

Theorem adh-minim-ax1

Proof