Metamath Proof Explorer

Theorem merco1lem18

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

Proof

Step	Hyp	Ref	Expression
1		merco1	$⊢ (((((ψ \to χ) \to ψ) \to ((ψ \to φ) \to ⊥)) \to ((ψ \to χ) \to ψ)) \to φ) \to ((φ \to (ψ \to χ)) \to ((ψ \to φ) \to (ψ \to χ)))$
2		merco1lem17	$⊢ ((((((ψ \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 χ))))$
3	1 2	ax-mp	$⊢ (((ψ \to χ) \to ψ) \to φ) \to ((φ \to (ψ \to χ)) \to ((ψ \to φ) \to (ψ \to χ)))$
4		merco1lem17	$⊢ ((((ψ \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 χ)))$
6		merco1lem5	$⊢ (((((((φ \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 ⊥)$
7		merco1lem3	$⊢ ((((((((φ \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 (ψ \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 ((ψ \to φ) \to (ψ \to χ)))) \to ⊥)) \to ((((((φ \to (ψ \to χ)) \to ((ψ \to φ) \to (ψ \to χ))) \to ⊥) \to (((ψ \to φ) \to ((φ \to (ψ \to χ)) \to ((ψ \to φ) \to (ψ \to χ)))) \to ⊥)) \to ⊥) \to ⊥)$
9		merco1lem5	$⊢ (((((φ \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 ((φ \to (ψ \to χ)) \to ((ψ \to φ) \to (ψ \to χ)))) \to ⊥)) \to ⊥) \to ⊥))$
10	8 9	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 ⊥)$
11		merco1lem4	$⊢ (((φ \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 ⊥))$
12	10 11	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 ⊥)$
13		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 χ)))))$
14		merco1lem2	$⊢ (((((((φ \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 (ψ \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 χ))))))$
15	13 14	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 (((ψ \to φ) \to ((φ \to (ψ \to χ)) \to ((ψ \to φ) \to (ψ \to χ)))) \to ((φ \to (ψ \to χ)) \to ((ψ \to φ) \to (ψ \to χ)))))$
16	12 15	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 χ))))$
17		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 χ))))$
18	16 17	ax-mp	$⊢ ((ψ \to φ) \to ((φ \to (ψ \to χ)) \to ((ψ \to φ) \to (ψ \to χ)))) \to ((φ \to (ψ \to χ)) \to ((ψ \to φ) \to (ψ \to χ)))$
19	5 18	ax-mp	$⊢ (φ \to (ψ \to χ)) \to ((ψ \to φ) \to (ψ \to χ))$