retbwax1

This theorem, along with retbwax2 , retbwax3 , and retbwax4 , shows that merco1 with ax-mp can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 18-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		merco1lem18	$⊢ (ψ \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ))$
2		merco1lem16	$⊢ ((ψ \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ))) \to ((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ)))$
3	1 2	ax-mp	$⊢ (ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))$
4		merco1lem15	$⊢ ((φ \to ψ) \to (φ \to χ)) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))$
5		merco1lem15	$⊢ (((φ \to ψ) \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		merco1lem18	$⊢ (((φ \to ψ) \to (φ \to χ)) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \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 χ))))$
9		merco1lem14	$⊢ ((((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to (φ \to χ))) \to (((ψ \to χ) \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 χ))))$
11		merco1lem14	$⊢ ((((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \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		merco1lem10	$⊢ ((((((((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ⊥) \to ⊥) \to ((((ψ \to χ) \to (φ \to χ)) \to φ) \to ⊥)) \to ((((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥)) \to (((φ \to χ) \to φ) \to ((((ψ \to χ) \to (((ψ \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		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 ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥)) \to (((((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ⊥)) \to ((((ψ \to χ) \to (φ \to χ)) \to φ) \to (((((ψ \to χ) \to (((ψ \to χ) \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	12 13	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 χ))))) \to ⊥) \to ⊥)) \to ((((ψ \to χ) \to (φ \to χ)) \to φ) \to (((((ψ \to χ) \to (((ψ \to χ) \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		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 ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ⊥)) \to (φ \to χ)) \to ((((ψ \to χ) \to (((ψ \to χ) \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	14 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 χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ⊥)) \to (φ \to χ)) \to ((((ψ \to χ) \to (((ψ \to χ) \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		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 ψ) \to (φ \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 χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (φ \to χ)) \to ((ψ \to χ) \to (φ \to χ))) \to (((((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ((ψ \to χ) \to (φ \to χ)))$
19	11 18	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 χ))$
20		merco1lem15	$⊢ (((((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ((ψ \to χ) \to (φ \to χ))) \to (((((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \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 χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))$
22		merco1lem10	$⊢ (((((((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))) \to ((((((((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))) \to (((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))))$
23		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 χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))) \to (((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))))) \to ((((((((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))) \to (((ψ \to χ) \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 ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))) \to (((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))$
25		merco1lem13	$⊢ ((((((((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))) \to (((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))))) \to ((((((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))) \to (((ψ \to χ) \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 ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to ⊥) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))) \to (((ψ \to χ) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \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 ψ) \to ((ψ \to χ) \to (φ \to χ))))) \to (((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))))$
28	10 27	ax-mp	$⊢ ((ψ \to χ) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ)))$
29	3 28	ax-mp	$⊢ (φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))$

Metamath Proof Explorer

Theorem retbwax1

Proof