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

Theorem necon3ai 2685
Description: Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon3ai.1
Assertion
Ref Expression
necon3ai

Proof of Theorem necon3ai
StepHypRef Expression
1 necon3ai.1 . . 3
2 nne 2658 . . 3
31, 2sylibr 212 . 2
43con2i 120 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652
This theorem is referenced by:  necon1ai  2688  necon3i  2697  disjsn2  4091  opelopabsb  4762  0nelxp  5032  fvunsn  6103  map0b  7477  mapdom3  7709  wemapso2OLD  7998  wemapso2lem  7999  cflim2  8664  isfin4-3  8716  fpwwe2lem13  9041  tskuni  9182  recextlem2  10205  hashprg  12460  eqsqrt2d  13201  gcd1  14170  gcdeq  14190  phimullem  14309  pcgcd1  14400  pc2dvds  14402  pockthlem  14423  ablfacrplem  17116  lbsextlem4  17807  znrrg  18604  obslbs  18761  opnfbas  20343  supfil  20396  itg1addlem4  22106  itg1addlem5  22107  dvdsmulf1o  23470  ppiub  23479  dchrelbas4  23518  lgsne0  23608  2sqlem8  23647  tgldimor  23893  nbcusgra  24463  uvtxnbgra  24493  wlkcpr  24529  vdgr1b  24904  frgraunss  24995  qqhval2  27963  derangsn  28614  subfacp1lem6  28629  cvmsss2  28719  fperdvper  31715  dvnmul  31740  wallispi  31852  fourierdlem56  31945  ax6e2ndeq  33332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-ne 2654
  Copyright terms: Public domain W3C validator