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

Theorem necon3ai 2591
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 2555 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
31, 2sylibr 204 . 2  |-  ( ph  ->  -.  A  =/=  B
)
43con2i 114 1  |-  ( A  =/=  B  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2551
This theorem is referenced by:  disjsn2  3813  opelopabsb  4407  0nelxp  4847  fvunsn  5865  map0b  6989  mapdom3  7216  wemapso2  7455  cflim2  8077  isfin4-3  8129  fpwwe2lem13  8451  tskuni  8592  recextlem2  9586  hashprg  11594  eqsqr2d  12100  gcd1  12960  gcdeq  12980  phimullem  13096  pcgcd1  13178  pc2dvds  13180  pockthlem  13201  ablfacrplem  15551  lbsextlem4  16161  znrrg  16770  obslbs  16881  opnfbas  17796  supfil  17849  itg1addlem4  19459  itg1addlem5  19460  dvdsmulf1o  20847  ppiub  20856  dchrelbas4  20895  lgsne0  20985  2sqlem8  21024  nbcusgra  21339  uvtxnbgra  21369  vdgr1b  21524  qqhval2  24166  derangsn  24636  subfacp1lem6  24651  cvmsss2  24741  wallispi  27488  frgraunss  27749  a9e2ndeq  27990
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-ne 2553
  Copyright terms: Public domain W3C validator