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

Theorem necon3ai 2677
Description: Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon3ai.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
necon3ai  |-  ( A  =/=  B  ->  -.  ph )

Proof of Theorem necon3ai
StepHypRef Expression
1 necon3ai.1 . . 3  |-  ( ph  ->  A  =  B )
2 nne 2651 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
31, 2sylibr 212 . 2  |-  ( ph  ->  -.  A  =/=  B
)
43con2i 120 1  |-  ( A  =/=  B  ->  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1370    =/= wne 2645
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 2647
This theorem is referenced by:  necon1ai  2680  necon3i  2689  disjsn2  4040  opelopabsb  4702  0nelxp  4970  fvunsn  6014  map0b  7356  mapdom3  7588  wemapso2OLD  7872  wemapso2lem  7873  cflim2  8538  isfin4-3  8590  fpwwe2lem13  8915  tskuni  9056  recextlem2  10073  hashprg  12268  eqsqr2d  12969  gcd1  13829  gcdeq  13849  phimullem  13967  pcgcd1  14056  pc2dvds  14058  pockthlem  14079  ablfacrplem  16683  lbsextlem4  17360  znrrg  18118  obslbs  18275  opnfbas  19542  supfil  19595  itg1addlem4  21305  itg1addlem5  21306  dvdsmulf1o  22662  ppiub  22671  dchrelbas4  22710  lgsne0  22800  2sqlem8  22839  tgldimor  23085  nbcusgra  23518  uvtxnbgra  23548  vdgr1b  23721  qqhval2  26551  derangsn  27197  subfacp1lem6  27212  cvmsss2  27302  wallispi  30008  wlkcpr  30433  frgraunss  30730  ax6e2ndeq  31581
  Copyright terms: Public domain W3C validator