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

Theorem necon3ai 2638
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 2602 . . 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 1652    =/= wne 2598
This theorem is referenced by:  disjsn2  3861  opelopabsb  4457  0nelxp  4898  fvunsn  5917  map0b  7044  mapdom3  7271  wemapso2  7513  cflim2  8135  isfin4-3  8187  fpwwe2lem13  8509  tskuni  8650  recextlem2  9645  hashprg  11658  eqsqr2d  12164  gcd1  13024  gcdeq  13044  phimullem  13160  pcgcd1  13242  pc2dvds  13244  pockthlem  13265  ablfacrplem  15615  lbsextlem4  16225  znrrg  16838  obslbs  16949  opnfbas  17866  supfil  17919  itg1addlem4  19583  itg1addlem5  19584  dvdsmulf1o  20971  ppiub  20980  dchrelbas4  21019  lgsne0  21109  2sqlem8  21148  nbcusgra  21464  uvtxnbgra  21494  vdgr1b  21667  qqhval2  24358  derangsn  24848  subfacp1lem6  24863  cvmsss2  24953  wallispi  27776  frgraunss  28312  a9e2ndeq  28573
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 2600
  Copyright terms: Public domain W3C validator