merco1lem17

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

Proof

Step	Hyp	Ref	Expression
1		merco1lem11	$⊢ (((φ \to ψ) \to φ) \to φ) \to ((((χ \to φ) \to (((φ \to ψ) \to φ) \to ⊥)) \to ⊥) \to φ)$
2		merco1lem7	$⊢ (((((((χ \to φ) \to (((φ \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 ψ) \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 ψ) \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 φ)) \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 ψ) \to φ) \to ⊥)) \to ⊥) \to φ)$
7	1 6	ax-mp	$⊢ (((χ \to φ) \to (((φ \to ψ) \to φ) \to ⊥)) \to ⊥) \to φ$
8		merco1	$⊢ ((((χ \to φ) \to (((φ \to ψ) \to φ) \to ⊥)) \to ⊥) \to φ) \to ((φ \to χ) \to (((φ \to ψ) \to φ) \to χ))$
9	7 8	ax-mp	$⊢ (φ \to χ) \to (((φ \to ψ) \to φ) \to χ)$
10		merco1lem11	$⊢ ((((φ \to χ) \to ⊥) \to (φ \to χ)) \to (φ \to χ)) \to (((((((φ \to ψ) \to φ) \to χ) \to φ) \to ((((φ \to χ) \to ⊥) \to (φ \to χ)) \to ⊥)) \to ⊥) \to (φ \to χ))$
11		merco1lem7	$⊢ ((((((((((φ \to ψ) \to φ) \to χ) \to φ) \to ((((φ \to χ) \to ⊥) \to (φ \to χ)) \to ⊥)) \to ⊥) \to (φ \to χ)) \to φ) \to ((((((φ \to χ) \to ⊥) \to (φ \to χ)) \to (φ \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		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 φ) \to χ) \to φ) \to ((((φ \to χ) \to ⊥) \to (φ \to χ)) \to ⊥)) \to ⊥) \to (φ \to χ))) \to ((((((φ \to χ) \to ⊥) \to (φ \to χ)) \to (φ \to χ)) \to (((((((φ \to ψ) \to φ) \to χ) \to φ) \to ((((φ \to χ) \to ⊥) \to (φ \to χ)) \to ⊥)) \to ⊥) \to (φ \to χ))) \to (((((((φ \to ψ) \to φ) \to χ) \to φ) \to ((((φ \to χ) \to ⊥) \to (φ \to χ)) \to ⊥)) \to ⊥) \to (φ \to χ))))$
13	11 12	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 χ) \to ⊥) \to (φ \to χ)) \to ⊥)) \to ⊥) \to (φ \to χ)))$
14		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 ψ) \to φ) \to χ) \to φ) \to ((((φ \to χ) \to ⊥) \to (φ \to χ)) \to ⊥)) \to ⊥) \to (φ \to χ)))) \to ((((((φ \to χ) \to ⊥) \to (φ \to χ)) \to (φ \to χ)) \to (((((((φ \to ψ) \to φ) \to χ) \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 χ))$
16	10 15	ax-mp	$⊢ ((((((φ \to ψ) \to φ) \to χ) \to φ) \to ((((φ \to χ) \to ⊥) \to (φ \to χ)) \to ⊥)) \to ⊥) \to (φ \to χ)$
17		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 χ)))$
18	16 17	ax-mp	$⊢ ((φ \to χ) \to (((φ \to ψ) \to φ) \to χ)) \to ((((φ \to χ) \to ⊥) \to (φ \to χ)) \to (((φ \to ψ) \to φ) \to χ))$
19	9 18	ax-mp	$⊢ (((φ \to χ) \to ⊥) \to (φ \to χ)) \to (((φ \to ψ) \to φ) \to χ)$
20		merco1lem16	$⊢ ((((φ \to χ) \to ⊥) \to (φ \to χ)) \to (((φ \to ψ) \to φ) \to χ)) \to ((((φ \to χ) \to ⊥) \to χ) \to (((φ \to ψ) \to φ) \to χ))$
21	19 20	ax-mp	$⊢ (((φ \to χ) \to ⊥) \to χ) \to (((φ \to ψ) \to φ) \to χ)$
22		merco1lem4	$⊢ (((τ \to φ) \to ((φ \to χ) \to ⊥)) \to χ) \to (((φ \to χ) \to ⊥) \to χ)$
23		merco1lem11	$⊢ ((((τ \to φ) \to ((φ \to χ) \to ⊥)) \to χ) \to (((φ \to χ) \to ⊥) \to χ)) \to (((((((φ \to ψ) \to φ) \to χ) \to φ) \to ((((τ \to φ) \to ((φ \to χ) \to ⊥)) \to χ) \to ⊥)) \to ⊥) \to (((φ \to χ) \to ⊥) \to χ))$
24	22 23	ax-mp	$⊢ ((((((φ \to ψ) \to φ) \to χ) \to φ) \to ((((τ \to φ) \to ((φ \to χ) \to ⊥)) \to χ) \to ⊥)) \to ⊥) \to (((φ \to χ) \to ⊥) \to χ)$
25		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 χ)))$
26	24 25	ax-mp	$⊢ ((((φ \to χ) \to ⊥) \to χ) \to (((φ \to ψ) \to φ) \to χ)) \to ((((τ \to φ) \to ((φ \to χ) \to ⊥)) \to χ) \to (((φ \to ψ) \to φ) \to χ))$
27	21 26	ax-mp	$⊢ (((τ \to φ) \to ((φ \to χ) \to ⊥)) \to χ) \to (((φ \to ψ) \to φ) \to χ)$
28		merco1	$⊢ ((((τ \to φ) \to ((φ \to χ) \to ⊥)) \to χ) \to (((φ \to ψ) \to φ) \to χ)) \to (((((φ \to ψ) \to φ) \to χ) \to τ) \to ((φ \to χ) \to τ))$
29	27 28	ax-mp	$⊢ ((((φ \to ψ) \to φ) \to χ) \to τ) \to ((φ \to χ) \to τ)$

Metamath Proof Explorer

Theorem merco1lem17

Proof