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

Theorem ax5 207
 Description: Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105. (Contributed by Mario Carneiro, 10-Oct-2014.)
Hypotheses
Ref Expression
ax5.1
ax5.2
Assertion
Ref Expression
ax5
Distinct variable group:   ,

Proof of Theorem ax5
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ax5.2 . . . . . 6
2 ax5.1 . . . . . . . 8
32ax4 150 . . . . . . 7
4 wal 134 . . . . . . . 8
5 wim 137 . . . . . . . . . 10
65, 2, 1wov 72 . . . . . . . . 9
76wl 66 . . . . . . . 8
84, 7wc 50 . . . . . . 7
93, 8adantl 56 . . . . . 6
106ax4 150 . . . . . . 7
113ax-cb1 29 . . . . . . 7
1210, 11adantr 55 . . . . . 6
131, 9, 12mpd 156 . . . . 5
14 wv 64 . . . . . 6
154, 14ax-17 105 . . . . . . 7
166, 14ax-hbl1 103 . . . . . . 7
174, 7, 14, 15, 16hbc 110 . . . . . 6
182wl 66 . . . . . . 7
192, 14ax-hbl1 103 . . . . . . 7
204, 18, 14, 15, 19hbc 110 . . . . . 6
218, 14, 11, 17, 20hbct 155 . . . . 5
2213, 21alrimi 182 . . . 4
2322ex 158 . . 3
24 wtru 43 . . 3