Metamath Proof Explorer

Theorem merco1lem14

Description: Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 . (Contributed by Anthony Hart, 18-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	merco1lem14	$⊢ (((φ \to ψ) \to ψ) \to χ) \to (φ \to χ)$

Proof

Step	Hyp	Ref	Expression
1		merco1lem13	$⊢ (((φ \to ψ) \to ((φ \to ψ) \to ψ)) \to ((φ \to ψ) \to ψ)) \to (φ \to ((φ \to ψ) \to ψ))$
2		merco1lem8	$⊢ ((((φ \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 ψ))$
3		merco1	$⊢ (((((φ \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 ψ))))$
4	2 3	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 ψ)))$
5		merco1lem9	$⊢ (((((φ \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 ψ)))$
6	4 5	ax-mp	$⊢ ((((φ \to ψ) \to ((φ \to ψ) \to ψ)) \to ((φ \to ψ) \to ψ)) \to (φ \to ((φ \to ψ) \to ψ))) \to (φ \to ((φ \to ψ) \to ψ))$
7	1 6	ax-mp	$⊢ φ \to ((φ \to ψ) \to ψ)$
8		merco1lem12	$⊢ (φ \to ((φ \to ψ) \to ψ)) \to ((((χ \to φ) \to (φ \to ⊥)) \to φ) \to ((φ \to ψ) \to ψ))$
9	7 8	ax-mp	$⊢ (((χ \to φ) \to (φ \to ⊥)) \to φ) \to ((φ \to ψ) \to ψ)$
10		merco1	$⊢ ((((χ \to φ) \to (φ \to ⊥)) \to φ) \to ((φ \to ψ) \to ψ)) \to ((((φ \to ψ) \to ψ) \to χ) \to (φ \to χ))$
11	9 10	ax-mp	$⊢ (((φ \to ψ) \to ψ) \to χ) \to (φ \to χ)$