Theorem merco1lem18 1499

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

Assertion

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

Proof of Theorem merco1lem18

Step	Hyp	Ref	Expression
1		merco1 1478	. . . 4 ⊢ ((((((ψ → χ) → ψ) → ((ψ → φ) → ⊥ )) → ((ψ → χ) → ψ)) → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))))
2		merco1lem17 1498	. . . 4 ⊢ (((((((ψ → χ) → ψ) → ((ψ → φ) → ⊥ )) → ((ψ → χ) → ψ)) → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ((((ψ → χ) → ψ) → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))))
3	1, 2	ax-mp 5	. . 3 ⊢ ((((ψ → χ) → ψ) → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))))
4		merco1lem17 1498	. . 3 ⊢ (((((ψ → χ) → ψ) → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))))
5	3, 4	ax-mp 5	. 2 ⊢ ((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))))
6		merco1lem5 1485	. . . . . . 7 ⊢ ((((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → ⊥ ) → ⊥ ) → (((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ))
7		merco1lem3 1483	. . . . . . 7 ⊢ (((((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → ⊥ ) → ⊥ ) → (((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ )) → (((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → ⊥ )))
8	6, 7	ax-mp 5	. . . . . 6 ⊢ (((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → ⊥ ))
9		merco1lem5 1485	. . . . . 6 ⊢ ((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → ⊥ )) → (((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → ⊥ )))
10	8, 9	ax-mp 5	. . . . 5 ⊢ (((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → ⊥ ))
11		merco1lem4 1484	. . . . 5 ⊢ ((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → ⊥ )) → (((ψ → φ) → (ψ → χ)) → ((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → ⊥ )))
12	10, 11	ax-mp 5	. . . 4 ⊢ (((ψ → φ) → (ψ → χ)) → ((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → ⊥ ))
13		merco1 1478	. . . . 5 ⊢ (((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → (ψ → φ)) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))))))
14		merco1lem2 1482	. . . . 5 ⊢ ((((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → (ψ → φ)) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))))) → ((((ψ → φ) → (ψ → χ)) → ((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → ⊥ )) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))))))
15	13, 14	ax-mp 5	. . . 4 ⊢ ((((ψ → φ) → (ψ → χ)) → ((((((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) → ⊥ ) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ⊥ )) → ⊥ ) → ⊥ )) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))))))
16	12, 15	ax-mp 5	. . 3 ⊢ (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))))
17		merco1lem9 1490	. . 3 ⊢ ((((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))))) → (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))))
18	16, 17	ax-mp 5	. 2 ⊢ (((ψ → φ) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))) → ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))))
19	5, 18	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:  retbwax1  1500