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

Theorem necon3ai 2499
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 2463 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
31, 2sylibr 203 . 2  |-  ( ph  ->  -.  A  =/=  B
)
43con2i 112 1  |-  ( A  =/=  B  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  disjsn2  3707  opelopabsb  4291  0nelxp  4733  fvunsn  5728  map0b  6822  mapdom3  7049  wemapso2  7283  cflim2  7905  isfin4-3  7957  ac9  8126  ac9s  8136  fpwwe2lem13  8280  tskuni  8421  recextlem2  9415  hashprg  11384  eqsqr2d  11868  gcd1  12727  gcdeq  12747  phimullem  12863  pcgcd1  12945  pc2dvds  12947  pockthlem  12968  ablfacrplem  15316  lbsextlem4  15930  znrrg  16535  obslbs  16646  opnfbas  17553  supfil  17606  itg1addlem4  19070  itg1addlem5  19071  dvdsmulf1o  20450  ppiub  20459  dchrelbas4  20498  lgsne0  20588  2sqlem8  20627  derangsn  23716  subfacp1lem6  23731  cvmsss2  23820  vdgr1b  23910  neiopne  25154  fvsnn  25217  wallispi  27922  nbcusgra  28298  uvtxnbgra  28306  a9e2ndeq  28624
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 177  df-ne 2461
  Copyright terms: Public domain W3C validator