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

Theorem necon3ai 2682
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 2655 . . 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 1398    =/= wne 2649
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 2651
This theorem is referenced by:  necon1ai  2685  necon3i  2694  disjsn2  4077  opelopabsb  4746  0nelxp  5016  fvunsn  6079  map0b  7450  mapdom3  7682  wemapso2OLD  7969  wemapso2lem  7970  cflim2  8634  isfin4-3  8686  fpwwe2lem13  9009  tskuni  9150  recextlem2  10176  hashprg  12444  eqsqrt2d  13283  gcd1  14254  gcdeq  14274  phimullem  14393  pcgcd1  14484  pc2dvds  14486  pockthlem  14507  ablfacrplem  17311  lbsextlem4  18002  znrrg  18777  obslbs  18934  opnfbas  20509  supfil  20562  itg1addlem4  22272  itg1addlem5  22273  dvdsmulf1o  23668  ppiub  23677  dchrelbas4  23716  lgsne0  23806  2sqlem8  23845  tgldimor  24094  nbcusgra  24665  uvtxnbgra  24695  wlkcpr  24731  vdgr1b  25106  frgraunss  25197  qqhval2  28197  derangsn  28878  subfacp1lem6  28893  cvmsss2  28983  fperdvper  31954  dvnmul  31979  wallispi  32091  fourierdlem56  32184  ax6e2ndeq  33726
  Copyright terms: Public domain W3C validator