Mathbox for Andrew Salmon < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  axc11next Structured version   Unicode version

Theorem axc11next 30919
 Description: This theorem shows that, given axext4 2449, we can derive a version of axc11n 2022. However, it is weaker than axc11n 2022 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 16-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
axc11next
Distinct variable group:   ,

Proof of Theorem axc11next
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ax-ext 2445 . . . . . 6
21alimi 1614 . . . . 5
3 ax-11 1791 . . . . . . 7
4 ax-9 1771 . . . . . . . . 9
5 bi2 198 . . . . . . . . . . 11
65alimi 1614 . . . . . . . . . 10
7 nfv 1683 . . . . . . . . . . 11
87stdpc5 1855 . . . . . . . . . 10
96, 8syl 16 . . . . . . . . 9
104, 9syl9 71 . . . . . . . 8
1110alimdv 1685 . . . . . . 7
123, 11syl5 32 . . . . . 6
1312sps 1814 . . . . 5
142, 13mpcom 36 . . . 4
1514axc4i 1846 . . 3
16 nfa1 1845 . . . . . . . 8
171619.23 1857 . . . . . . 7
18 19.8a 1806 . . . . . . . . 9
19 elequ2 1772 . . . . . . . . . 10
2019cbvexv 1997 . . . . . . . . 9
2118, 20sylib 196 . . . . . . . 8
22 nfv 1683 . . . . . . . . 9
2322, 7, 4cbv3 1984 . . . . . . . 8
2421, 23imim12i 57 . . . . . . 7
2517, 24sylbi 195 . . . . . 6
2625alimi 1614 . . . . 5
2726alcoms 1792 . . . 4
2827alrimiv 1695 . . 3
29 nfa1 1845 . . . . . . . 8
302919.23 1857 . . . . . . 7
31 ax-9 1771 . . . . . . . . . 10
3231spimv 1978 . . . . . . . . 9
3318, 32imim12i 57 . . . . . . . 8
34 19.8a 1806 . . . . . . . . . 10
35 elequ2 1772 . . . . . . . . . . 11
3635cbvexv 1997 . . . . . . . . . 10
3734, 36sylib 196 . . . . . . . . 9
38 sp 1808 . . . . . . . . 9
3937, 38imim12i 57 . . . . . . . 8
4033, 39impbid 191 . . . . . . 7
4130, 40sylbi 195 . . . . . 6
4241alimi 1614 . . . . 5
4342alcoms 1792 . . . 4
4443axc4i 1846 . . 3
4515, 28, 443syl 20 . 2
46 axext4 2449 . . 3
4746albii 1620 . 2
48 axext4 2449 . . 3
4948albii 1620 . 2
5045, 47, 493imtr4i 266 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184  wal 1377   wceq 1379  wex 1596   wcel 1767 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator