merco2

Description: A single axiom for propositional calculus discovered by C. A. Meredith.

This axiom has 19 symbols, sans auxiliaries. See notes in merco1 . (Contributed by Anthony Hart, 7-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	merco2	$⊢ ((φ \to ψ) \to ((⊥ \to χ) \to θ)) \to ((θ \to φ) \to (τ \to (η \to φ)))$

Proof

Step	Hyp	Ref	Expression
1		falim	$⊢ ⊥ \to χ$
2		pm2.04	$⊢ ((φ \to ψ) \to ((⊥ \to χ) \to θ)) \to ((⊥ \to χ) \to ((φ \to ψ) \to θ))$
3	1 2	mpi	$⊢ ((φ \to ψ) \to ((⊥ \to χ) \to θ)) \to ((φ \to ψ) \to θ)$
4		jarl	$⊢ ((φ \to ψ) \to θ) \to (\neg φ \to θ)$
5		idd	$⊢ ((φ \to ψ) \to θ) \to (θ \to θ)$
6	4 5	jad	$⊢ ((φ \to ψ) \to θ) \to ((φ \to θ) \to θ)$
7		looinv	$⊢ ((φ \to θ) \to θ) \to ((θ \to φ) \to φ)$
8	3 6 7	3syl	$⊢ ((φ \to ψ) \to ((⊥ \to χ) \to θ)) \to ((θ \to φ) \to φ)$
9	8	a1dd	$⊢ ((φ \to ψ) \to ((⊥ \to χ) \to θ)) \to ((θ \to φ) \to (τ \to φ))$
10	9	a1i	$⊢ η \to (((φ \to ψ) \to ((⊥ \to χ) \to θ)) \to ((θ \to φ) \to (τ \to φ)))$
11	10	com4l	$⊢ ((φ \to ψ) \to ((⊥ \to χ) \to θ)) \to ((θ \to φ) \to (τ \to (η \to φ)))$

Metamath Proof Explorer

Theorem merco2

Proof