Theorem retbwax2 1481

Description: tbw-ax2 1466 rederived from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
retbwax2	⊢ (φ → (ψ → φ))

Proof of Theorem retbwax2

Step	Hyp	Ref	Expression
1		merco1lem1 1479	. . . 4 ⊢ (((((φ → φ) → φ) → (φ → ⊥ )) → φ) → ( ⊥ → φ))
2		merco1 1478	. . . 4 ⊢ ((((((φ → φ) → φ) → (φ → ⊥ )) → φ) → ( ⊥ → φ)) → ((( ⊥ → φ) → (φ → φ)) → (φ → (φ → φ))))
3	1, 2	ax-mp 5	. . 3 ⊢ ((( ⊥ → φ) → (φ → φ)) → (φ → (φ → φ)))
4		merco1 1478	. . . 4 ⊢ (((((φ → (φ → φ)) → (φ → ⊥ )) → (φ → ⊥ )) → ⊥ ) → (( ⊥ → φ) → (φ → φ)))
5		merco1 1478	. . . 4 ⊢ ((((((φ → (φ → φ)) → (φ → ⊥ )) → (φ → ⊥ )) → ⊥ ) → (( ⊥ → φ) → (φ → φ))) → (((( ⊥ → φ) → (φ → φ)) → (φ → (φ → φ))) → (φ → (φ → (φ → φ)))))
6	4, 5	ax-mp 5	. . 3 ⊢ (((( ⊥ → φ) → (φ → φ)) → (φ → (φ → φ))) → (φ → (φ → (φ → φ))))
7	3, 6	ax-mp 5	. 2 ⊢ (φ → (φ → (φ → φ)))
8		merco1lem1 1479	. . . 4 ⊢ (((((ψ → φ) → φ) → (φ → ⊥ )) → φ) → ( ⊥ → φ))
9		merco1 1478	. . . 4 ⊢ ((((((ψ → φ) → φ) → (φ → ⊥ )) → φ) → ( ⊥ → φ)) → ((( ⊥ → φ) → (ψ → φ)) → (φ → (ψ → φ))))
10	8, 9	ax-mp 5	. . 3 ⊢ ((( ⊥ → φ) → (ψ → φ)) → (φ → (ψ → φ)))
11		merco1 1478	. . . 4 ⊢ (((((φ → (ψ → φ)) → (ψ → ⊥ )) → ((φ → (φ → (φ → φ))) → ⊥ )) → ⊥ ) → (( ⊥ → φ) → (ψ → φ)))
12		merco1 1478	. . . 4 ⊢ ((((((φ → (ψ → φ)) → (ψ → ⊥ )) → ((φ → (φ → (φ → φ))) → ⊥ )) → ⊥ ) → (( ⊥ → φ) → (ψ → φ))) → (((( ⊥ → φ) → (ψ → φ)) → (φ → (ψ → φ))) → ((φ → (φ → (φ → φ))) → (φ → (ψ → φ)))))
13	11, 12	ax-mp 5	. . 3 ⊢ (((( ⊥ → φ) → (ψ → φ)) → (φ → (ψ → φ))) → ((φ → (φ → (φ → φ))) → (φ → (ψ → φ))))
14	10, 13	ax-mp 5	. 2 ⊢ ((φ → (φ → (φ → φ))) → (φ → (ψ → φ)))
15	7, 14	ax-mp 5	1 ⊢ (φ → (ψ → φ))

This proof depends on syntax axioms:   → wi 4   ⊥ wfal 1317

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

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

This theorem is used by:  merco1lem2  1482  merco1lem3  1483  retbwax3  1488