Metamath Proof Explorer


Theorem tarski-bernays-ax2

Description: Derivation of ax-2 from the Tarski-Bernays axiom set { ax-1 , imim1 , peirce }. Note that no inference rule other than ax-mp is used in this proof. This proof establishes a circle of equivalence: From { impsingle }, { ax-1 , imim1 , peirce } was proved. From { ax-1 , imim1 , peirce }, { ax-1 , ax-2 and peirce } was proved. From { ax-1 , ax-2 and peirce }, { impsingle } was proved. Therefore, the theorems that can be proved by selecting any one of these three distinct axiom sets must be equivalent. Prover9 and mmj2 were used to help constuct this proof. (Contributed by Larry Lesyna and Jeffrey P. Machado, 1-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion tarski-bernays-ax2 φ ψ χ φ ψ φ χ

Proof

Step Hyp Ref Expression
1 peirce φ χ χ φ χ φ χ
2 ax-1 φ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ
3 1 2 ax-mp φ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ
4 imim1 φ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ
5 3 4 ax-mp φ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ
6 peirce φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ
7 imim1 φ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ
8 imim1 φ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ
9 7 8 ax-mp φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ
10 6 9 ax-mp φ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ
11 5 10 ax-mp φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ
12 imim1 ψ χ χ φ χ φ χ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ
13 imim1 ψ χ χ φ χ φ χ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ χ φ χ ψ χ χ φ χ φ χ
14 12 13 ax-mp φ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ χ φ χ ψ χ χ φ χ φ χ
15 11 14 ax-mp ψ χ χ φ χ φ χ χ φ χ ψ χ χ φ χ φ χ
16 imim1 φ χ χ ψ χ χ ψ χ χ φ χ φ χ χ φ χ
17 imim1 φ χ χ ψ χ χ ψ χ χ φ χ φ χ χ φ χ ψ χ χ φ χ φ χ χ φ χ ψ χ χ φ χ φ χ φ χ χ ψ χ χ ψ χ χ φ χ φ χ
18 16 17 ax-mp ψ χ χ φ χ φ χ χ φ χ ψ χ χ φ χ φ χ φ χ χ ψ χ χ ψ χ χ φ χ φ χ
19 15 18 ax-mp φ χ χ ψ χ χ ψ χ χ φ χ φ χ
20 imim1 ψ χ φ χ φ χ χ ψ χ χ
21 imim1 ψ χ φ χ φ χ χ ψ χ χ φ χ χ ψ χ χ ψ χ χ φ χ φ χ ψ χ φ χ ψ χ χ φ χ φ χ
22 20 21 ax-mp φ χ χ ψ χ χ ψ χ χ φ χ φ χ ψ χ φ χ ψ χ χ φ χ φ χ
23 19 22 ax-mp ψ χ φ χ ψ χ χ φ χ φ χ
24 peirce ψ χ χ φ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ
25 imim1 ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ
26 imim1 ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ
27 25 26 ax-mp ψ χ χ φ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ
28 24 27 ax-mp ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ
29 imim1 ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ
30 imim1 ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ
31 29 30 ax-mp ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ
32 28 31 ax-mp ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ
33 ax-1 ψ χ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ
34 imim1 ψ χ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ
35 33 34 ax-mp ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ
36 32 35 ax-mp ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ
37 imim1 ψ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ φ χ φ χ
38 imim1 ψ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ ψ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ
39 37 38 ax-mp ψ χ χ φ χ φ χ φ χ ψ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ ψ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ
40 imim1 ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ
41 imim1 ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ ψ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ
42 40 41 ax-mp ψ χ χ φ χ φ χ φ χ ψ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ ψ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ
43 39 42 ax-mp ψ χ χ φ χ ψ χ χ φ χ φ χ φ χ ψ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ
44 36 43 ax-mp ψ χ φ χ ψ χ χ φ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ
45 23 44 ax-mp ψ χ χ φ χ ψ χ φ χ φ χ
46 imim1 φ ψ χ ψ χ χ φ χ
47 imim1 φ ψ χ ψ χ χ φ χ ψ χ χ φ χ ψ χ φ χ φ χ φ ψ χ ψ χ φ χ φ χ
48 46 47 ax-mp ψ χ χ φ χ ψ χ φ χ φ χ φ ψ χ ψ χ φ χ φ χ
49 45 48 ax-mp φ ψ χ ψ χ φ χ φ χ
50 peirce ψ χ φ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ
51 imim1 ψ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ
52 imim1 ψ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ
53 51 52 ax-mp ψ χ φ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ
54 50 53 ax-mp ψ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ
55 imim1 ψ χ φ χ φ χ ψ χ φ χ ψ χ φ χ φ χ ψ χ φ χ φ χ φ χ
56 imim1 ψ χ φ χ φ χ ψ χ φ χ ψ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ ψ χ φ χ ψ χ φ χ φ χ φ χ
57 55 56 ax-mp ψ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ ψ χ φ χ ψ χ φ χ φ χ φ χ
58 54 57 ax-mp ψ χ φ χ φ χ ψ χ φ χ ψ χ φ χ φ χ φ χ
59 ax-1 ψ χ φ χ ψ χ φ χ φ χ ψ χ φ χ
60 imim1 ψ χ φ χ ψ χ φ χ φ χ ψ χ φ χ ψ χ φ χ φ χ ψ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ ψ χ φ χ φ χ φ χ
61 59 60 ax-mp ψ χ φ χ φ χ ψ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ ψ χ φ χ φ χ φ χ
62 58 61 ax-mp ψ χ φ χ ψ χ φ χ φ χ φ χ
63 imim1 φ ψ χ ψ χ φ χ φ χ ψ χ φ χ φ χ φ χ φ ψ χ φ χ
64 imim1 φ ψ χ ψ χ φ χ φ χ ψ χ φ χ φ χ φ χ φ ψ χ φ χ ψ χ φ χ φ χ φ χ φ ψ χ φ χ ψ χ φ χ φ ψ χ φ χ φ ψ χ ψ χ φ χ φ χ ψ χ φ χ φ ψ χ φ χ
65 63 64 ax-mp ψ χ φ χ φ χ φ χ φ ψ χ φ χ ψ χ φ χ φ ψ χ φ χ φ ψ χ ψ χ φ χ φ χ ψ χ φ χ φ ψ χ φ χ
66 imim1 ψ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ φ ψ χ φ χ ψ χ φ χ φ ψ χ φ χ
67 imim1 ψ χ φ χ ψ χ φ χ φ χ φ χ ψ χ φ χ φ χ φ χ φ ψ χ φ χ ψ χ φ χ φ ψ χ φ χ ψ χ φ χ φ χ φ χ φ ψ χ φ χ ψ χ φ χ φ ψ χ φ χ φ ψ χ ψ χ φ χ φ χ ψ χ φ χ φ ψ χ φ χ ψ χ φ χ ψ χ φ χ φ χ φ χ φ ψ χ ψ χ φ χ φ χ ψ χ φ χ φ ψ χ φ χ
68 66 67 ax-mp ψ χ φ χ φ χ φ χ φ ψ χ φ χ ψ χ φ χ φ ψ χ φ χ φ ψ χ ψ χ φ χ φ χ ψ χ φ χ φ ψ χ φ χ ψ χ φ χ ψ χ φ χ φ χ φ χ φ ψ χ ψ χ φ χ φ χ ψ χ φ χ φ ψ χ φ χ
69 65 68 ax-mp ψ χ φ χ ψ χ φ χ φ χ φ χ φ ψ χ ψ χ φ χ φ χ ψ χ φ χ φ ψ χ φ χ
70 62 69 ax-mp φ ψ χ ψ χ φ χ φ χ ψ χ φ χ φ ψ χ φ χ
71 49 70 ax-mp ψ χ φ χ φ ψ χ φ χ
72 imim1 φ ψ ψ χ φ χ
73 imim1 φ ψ ψ χ φ χ ψ χ φ χ φ ψ χ φ χ φ ψ φ ψ χ φ χ
74 72 73 ax-mp ψ χ φ χ φ ψ χ φ χ φ ψ φ ψ χ φ χ
75 71 74 ax-mp φ ψ φ ψ χ φ χ
76 peirce φ ψ χ φ χ φ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ
77 imim1 φ ψ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ φ χ φ ψ χ φ χ φ χ
78 imim1 φ ψ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ
79 77 78 ax-mp φ ψ χ φ χ φ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ
80 76 79 ax-mp φ ψ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ
81 imim1 φ ψ χ φ χ φ ψ χ φ ψ χ φ χ φ ψ χ φ χ φ χ
82 imim1 φ ψ χ φ χ φ ψ χ φ ψ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ ψ χ φ ψ χ φ χ φ χ
83 81 82 ax-mp φ ψ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ ψ χ φ ψ χ φ χ φ χ
84 80 83 ax-mp φ ψ χ φ χ φ ψ χ φ ψ χ φ χ φ χ
85 ax-1 φ ψ χ φ ψ χ φ χ φ ψ χ
86 imim1 φ ψ χ φ ψ χ φ χ φ ψ χ φ ψ χ φ χ φ ψ χ φ ψ χ φ χ φ χ φ ψ χ φ ψ χ φ χ φ χ
87 85 86 ax-mp φ ψ χ φ χ φ ψ χ φ ψ χ φ χ φ χ φ ψ χ φ ψ χ φ χ φ χ
88 84 87 ax-mp φ ψ χ φ ψ χ φ χ φ χ
89 imim1 φ ψ φ ψ χ φ χ φ ψ χ φ χ φ χ φ ψ φ χ
90 imim1 φ ψ φ ψ χ φ χ φ ψ χ φ χ φ χ φ ψ φ χ φ ψ χ φ χ φ χ φ ψ φ χ φ ψ χ φ ψ φ χ φ ψ φ ψ χ φ χ φ ψ χ φ ψ φ χ
91 89 90 ax-mp φ ψ χ φ χ φ χ φ ψ φ χ φ ψ χ φ ψ φ χ φ ψ φ ψ χ φ χ φ ψ χ φ ψ φ χ
92 imim1 φ ψ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ φ ψ φ χ φ ψ χ φ ψ φ χ
93 imim1 φ ψ χ φ ψ χ φ χ φ χ φ ψ χ φ χ φ χ φ ψ φ χ φ ψ χ φ ψ φ χ φ ψ χ φ χ φ χ φ ψ φ χ φ ψ χ φ ψ φ χ φ ψ φ ψ χ φ χ φ ψ χ φ ψ φ χ φ ψ χ φ ψ χ φ χ φ χ φ ψ φ ψ χ φ χ φ ψ χ φ ψ φ χ
94 92 93 ax-mp φ ψ χ φ χ φ χ φ ψ φ χ φ ψ χ φ ψ φ χ φ ψ φ ψ χ φ χ φ ψ χ φ ψ φ χ φ ψ χ φ ψ χ φ χ φ χ φ ψ φ ψ χ φ χ φ ψ χ φ ψ φ χ
95 91 94 ax-mp φ ψ χ φ ψ χ φ χ φ χ φ ψ φ ψ χ φ χ φ ψ χ φ ψ φ χ
96 88 95 ax-mp φ ψ φ ψ χ φ χ φ ψ χ φ ψ φ χ
97 75 96 ax-mp φ ψ χ φ ψ φ χ