Higher-Order Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax7 Unicode version

Theorem ax7 209
 Description: Axiom of Quantifier Commutation. Axiom scheme C6' in [Megill] p. 448 (p. 16 of the preprint). (Contributed by Mario Carneiro, 10-Oct-2014.)
Hypothesis
Ref Expression
ax7.1
Assertion
Ref Expression
ax7
Distinct variable group:   ,,

Proof of Theorem ax7
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 wal 134 . . . . . . . 8
2 ax7.1 . . . . . . . . 9
32wl 66 . . . . . . . 8
41, 3wc 50 . . . . . . 7
54ax4 150 . . . . . 6
62ax4 150 . . . . . 6
75, 6syl 16 . . . . 5
84wl 66 . . . . . 6
9 wv 64 . . . . . 6
101, 9ax-17 105 . . . . . 6
114, 9ax-hbl1 103 . . . . . 6
121, 8, 9, 10, 11hbc 110 . . . . 5
137, 12alrimi 182 . . . 4
141, 9ax-17 105 . . . . 5
152, 9ax-hbl1 103 . . . . . . 7
161, 3, 9, 14, 15hbc 110 . . . . . 6
174, 9, 16hbl 112 . . . . 5
181, 8, 9, 14, 17hbc 110 . . . 4
1913, 18alrimi 182 . . 3
20 wtru 43 . . 3