Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lpni Structured version   Unicode version

Theorem lpni 25756
 Description: For any line, there exists a point not on the line. (Contributed by Jeff Hankins, 15-Aug-2009.)
Hypothesis
Ref Expression
lpni.1
Assertion
Ref Expression
lpni
Distinct variable groups:   ,   ,   ,

Proof of Theorem lpni
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lpni.1 . . . 4
21tncp 25755 . . 3
3 eleq2 2502 . . . . . . . . . 10
4 eleq2 2502 . . . . . . . . . 10
5 eleq2 2502 . . . . . . . . . 10
63, 4, 53anbi123d 1335 . . . . . . . . 9
76notbid 295 . . . . . . . 8
87rspccv 3185 . . . . . . 7
9 eleq1 2501 . . . . . . . . . . . 12
109notbid 295 . . . . . . . . . . 11
1110rspcev 3188 . . . . . . . . . 10
1211ex 435 . . . . . . . . 9
13 eleq1 2501 . . . . . . . . . . . 12
1413notbid 295 . . . . . . . . . . 11
1514rspcev 3188 . . . . . . . . . 10
1615ex 435 . . . . . . . . 9
17 eleq1 2501 . . . . . . . . . . . 12
1817notbid 295 . . . . . . . . . . 11
1918rspcev 3188 . . . . . . . . . 10
2019ex 435 . . . . . . . . 9
2112, 16, 203jaao 1332 . . . . . . . 8
22 3ianor 999 . . . . . . . 8
23 df-nel 2628 . . . . . . . . 9
2423rexbii 2934 . . . . . . . 8
2521, 22, 243imtr4g 273 . . . . . . 7
268, 25syl9r 74 . . . . . 6
27263expia 1207 . . . . 5
2827rexlimdv 2922 . . . 4
2928rexlimivv 2929 . . 3
302, 29syl 17 . 2
3130imp 430 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 370   w3o 981   w3a 982   wceq 1437   wcel 1870   wnel 2626  wral 2782  wrex 2783  cuni 4222  cplig 25752 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-v 3089  df-uni 4223  df-plig 25753 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator