Theorem retbwax1 1500

Description: tbw-ax1 1465 rederived from merco1 1478.

This theorem, along with retbwax2 1481, retbwax3 1488, and retbwax4 1480, shows that merco1 1478 with ax-mp 5 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.)

Assertion

Ref	Expression
retbwax1	⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ)))

Proof of Theorem retbwax1

Step	Hyp	Ref	Expression
1		merco1lem18 1499	. . 3 ⊢ ((ψ → (φ → χ)) → ((φ → ψ) → (φ → χ)))
2		merco1lem16 1497	. . 3 ⊢ (((ψ → (φ → χ)) → ((φ → ψ) → (φ → χ))) → ((ψ → χ) → ((φ → ψ) → (φ → χ))))
3	1, 2	ax-mp 5	. 2 ⊢ ((ψ → χ) → ((φ → ψ) → (φ → χ)))
4		merco1lem15 1496	. . . . . 6 ⊢ (((φ → ψ) → (φ → χ)) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))
5		merco1lem15 1496	. . . . . 6 ⊢ ((((φ → ψ) → (φ → χ)) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))) → (((φ → ψ) → (φ → χ)) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))))
6	4, 5	ax-mp 5	. . . . 5 ⊢ (((φ → ψ) → (φ → χ)) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))
7		merco1lem18 1499	. . . . 5 ⊢ ((((φ → ψ) → (φ → χ)) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ((((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → (φ → χ))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))))
8	6, 7	ax-mp 5	. . . 4 ⊢ ((((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → (φ → χ))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))
9		merco1lem14 1495	. . . 4 ⊢ (((((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → (φ → χ))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))))
10	8, 9	ax-mp 5	. . 3 ⊢ ((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))
11		merco1lem14 1495	. . . . . 6 ⊢ (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (φ → χ)) → ((ψ → χ) → (φ → χ)))
12		merco1lem10 1491	. . . . . . . . 9 ⊢ (((((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ⊥ ) → ⊥ ) → ((((ψ → χ) → (φ → χ)) → φ) → ⊥ )) → ((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ )) → (((φ → χ) → φ) → ((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ )))
13		merco1 1478	. . . . . . . . 9 ⊢ ((((((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ⊥ ) → ⊥ ) → ((((ψ → χ) → (φ → χ)) → φ) → ⊥ )) → ((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ )) → (((φ → χ) → φ) → ((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ))) → (((((φ → χ) → φ) → ((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ )) → (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ⊥ )) → ((((ψ → χ) → (φ → χ)) → φ) → (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ⊥ ))))
14	12, 13	ax-mp 5	. . . . . . . 8 ⊢ (((((φ → χ) → φ) → ((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ )) → (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ⊥ )) → ((((ψ → χ) → (φ → χ)) → φ) → (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ⊥ )))
15		merco1 1478	. . . . . . . 8 ⊢ ((((((φ → χ) → φ) → ((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ )) → (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ⊥ )) → ((((ψ → χ) → (φ → χ)) → φ) → (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ⊥ ))) → ((((((ψ → χ) → (φ → χ)) → φ) → (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ⊥ )) → (φ → χ)) → ((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (φ → χ))))
16	14, 15	ax-mp 5	. . . . . . 7 ⊢ ((((((ψ → χ) → (φ → χ)) → φ) → (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ⊥ )) → (φ → χ)) → ((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (φ → χ)))
17		merco1 1478	. . . . . . 7 ⊢ (((((((ψ → χ) → (φ → χ)) → φ) → (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ⊥ )) → (φ → χ)) → ((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (φ → χ))) → ((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (φ → χ)) → ((ψ → χ) → (φ → χ))) → (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((ψ → χ) → (φ → χ)))))
18	16, 17	ax-mp 5	. . . . . 6 ⊢ ((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (φ → χ)) → ((ψ → χ) → (φ → χ))) → (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((ψ → χ) → (φ → χ))))
19	11, 18	ax-mp 5	. . . . 5 ⊢ (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((ψ → χ) → (φ → χ)))
20		merco1lem15 1496	. . . . 5 ⊢ ((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((ψ → χ) → (φ → χ))) → (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))
21	19, 20	ax-mp 5	. . . 4 ⊢ (((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))
22		merco1lem10 1491	. . . . . 6 ⊢ ((((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))) → ((((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))))
23		merco1lem9 1490	. . . . . 6 ⊢ (((((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))) → ((((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))))) → ((((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))))
24	22, 23	ax-mp 5	. . . . 5 ⊢ ((((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))))
25		merco1lem13 1494	. . . . 5 ⊢ (((((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))) → ((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))))
26	24, 25	ax-mp 5	. . . 4 ⊢ ((((((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → ⊥ ) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))) → (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))))
27	21, 26	ax-mp 5	. . 3 ⊢ (((ψ → χ) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))) → (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ)))))
28	10, 27	ax-mp 5	. 2 ⊢ (((ψ → χ) → ((φ → ψ) → (φ → χ))) → ((φ → ψ) → ((ψ → χ) → (φ → χ))))
29	3, 28	ax-mp 5	1 ⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ)))

Syntax hints:   → wi 4   ⊥ wfal 1317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-tru 1319  df-fal 1320

This theorem is referenced by: (None)