Metamath Proof Explorer


Theorem retbwax2

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

Ref Expression
Assertion retbwax2 φ ψ φ

Proof

Step Hyp Ref Expression
1 merco1lem1 φ φ φ φ φ φ
2 merco1 φ φ φ φ φ φ φ φ φ φ φ φ
3 1 2 ax-mp φ φ φ φ φ φ
4 merco1 φ φ φ φ φ φ φ φ
5 merco1 φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ φ
6 4 5 ax-mp φ φ φ φ φ φ φ φ φ φ
7 3 6 ax-mp φ φ φ φ
8 merco1lem1 ψ φ φ φ φ φ
9 merco1 ψ φ φ φ φ φ φ ψ φ φ ψ φ
10 8 9 ax-mp φ ψ φ φ ψ φ
11 merco1 φ ψ φ ψ φ φ φ φ φ ψ φ
12 merco1 φ ψ φ ψ φ φ φ φ φ ψ φ φ ψ φ φ ψ φ φ φ φ φ φ ψ φ
13 11 12 ax-mp φ ψ φ φ ψ φ φ φ φ φ φ ψ φ
14 10 13 ax-mp φ φ φ φ φ ψ φ
15 7 14 ax-mp φ ψ φ