Metamath Proof Explorer


Theorem merco1lem17

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

Ref Expression
Assertion merco1lem17 φ ψ φ χ τ φ χ τ

Proof

Step Hyp Ref Expression
1 merco1lem11 φ ψ φ φ χ φ φ ψ φ φ
2 merco1lem7 χ φ φ ψ φ φ φ φ ψ φ φ χ φ φ ψ φ φ φ φ ψ φ φ
3 merco1 χ φ φ ψ φ φ φ φ ψ φ φ χ φ φ ψ φ φ φ φ ψ φ φ φ ψ φ φ χ φ φ ψ φ φ φ ψ φ φ χ φ φ ψ φ φ χ φ φ ψ φ φ
4 2 3 ax-mp φ ψ φ φ χ φ φ ψ φ φ φ ψ φ φ χ φ φ ψ φ φ χ φ φ ψ φ φ
5 merco1lem9 φ ψ φ φ χ φ φ ψ φ φ φ ψ φ φ χ φ φ ψ φ φ χ φ φ ψ φ φ φ ψ φ φ χ φ φ ψ φ φ χ φ φ ψ φ φ
6 4 5 ax-mp φ ψ φ φ χ φ φ ψ φ φ χ φ φ ψ φ φ
7 1 6 ax-mp χ φ φ ψ φ φ
8 merco1 χ φ φ ψ φ φ φ χ φ ψ φ χ
9 7 8 ax-mp φ χ φ ψ φ χ
10 merco1lem11 φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ
11 merco1lem7 φ ψ φ χ φ φ χ φ χ φ χ φ φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ φ φ χ φ χ φ χ
12 merco1 φ ψ φ χ φ φ χ φ χ φ χ φ φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ φ φ χ φ χ φ χ φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ
13 11 12 ax-mp φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ
14 merco1lem9 φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ
15 13 14 ax-mp φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ φ ψ φ χ φ φ χ φ χ φ χ
16 10 15 ax-mp φ ψ φ χ φ φ χ φ χ φ χ
17 merco1 φ ψ φ χ φ φ χ φ χ φ χ φ χ φ ψ φ χ φ χ φ χ φ ψ φ χ
18 16 17 ax-mp φ χ φ ψ φ χ φ χ φ χ φ ψ φ χ
19 9 18 ax-mp φ χ φ χ φ ψ φ χ
20 merco1lem4 τ φ φ χ χ φ χ χ
21 merco1lem16 φ χ φ χ φ ψ φ χ φ χ χ φ ψ φ χ
22 19 20 21 mpsyl τ φ φ χ χ φ ψ φ χ
23 merco1 τ φ φ χ χ φ ψ φ χ φ ψ φ χ τ φ χ τ
24 22 23 ax-mp φ ψ φ χ τ φ χ τ