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 φψχφψφχ