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

Theorem axc11next 36827
 Description: This theorem shows that, given axext4 2455, we can derive a version of axc11n 2157. However, it is weaker than axc11n 2157 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 2451 . . . . . 6
21alimi 1692 . . . . 5
3 ax-11 1937 . . . . . . 7
4 ax9 1917 . . . . . . . . 9
5 biimpr 203 . . . . . . . . . . 11
65alimi 1692 . . . . . . . . . 10
7 stdpc5v 1793 . . . . . . . . . 10
86, 7syl 17 . . . . . . . . 9
94, 8syl9 72 . . . . . . . 8
109alimdv 1771 . . . . . . 7
113, 10syl5 32 . . . . . 6
1211sps 1963 . . . . 5
132, 12mpcom 36 . . . 4
1413axc4i 2000 . . 3
15 nfa1 1999 . . . . . . . 8
161519.23 2013 . . . . . . 7
17 19.8a 1955 . . . . . . . . 9
18 elequ2 1918 . . . . . . . . . 10
1918cbvexv 2130 . . . . . . . . 9
2017, 19sylib 201 . . . . . . . 8
214cbvalivw 1858 . . . . . . . 8
2220, 21imim12i 58 . . . . . . 7
2316, 22sylbi 200 . . . . . 6
2423alimi 1692 . . . . 5
2524alcoms 1938 . . . 4
2625alrimiv 1781 . . 3
27 nfa1 1999 . . . . . . . 8
282719.23 2013 . . . . . . 7
29 ax9 1917 . . . . . . . . . 10
3029spimv 2114 . . . . . . . . 9
3117, 30imim12i 58 . . . . . . . 8
32 19.8a 1955 . . . . . . . . . 10
33 elequ2 1918 . . . . . . . . . . 11
3433cbvexv 2130 . . . . . . . . . 10
3532, 34sylib 201 . . . . . . . . 9
36 sp 1957 . . . . . . . . 9
3735, 36imim12i 58 . . . . . . . 8
3831, 37impbid 195 . . . . . . 7
3928, 38sylbi 200 . . . . . 6
4039alimi 1692 . . . . 5
4140alcoms 1938 . . . 4
4241axc4i 2000 . . 3
4314, 26, 423syl 18 . 2
44 axext4 2455 . . 3
4544albii 1699 . 2
46 axext4 2455 . . 3
4746albii 1699 . 2
4843, 45, 473imtr4i 274 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189  wal 1450   wceq 1452  wex 1671   wcel 1904 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451 This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator