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

Theorem necon3ai 2695
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 2668 . . 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 1379    =/= wne 2662
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 2664
This theorem is referenced by:  necon1ai  2698  necon3i  2707  disjsn2  4095  opelopabsb  4763  0nelxp  5033  fvunsn  6104  map0b  7469  mapdom3  7701  wemapso2OLD  7989  wemapso2lem  7990  cflim2  8655  isfin4-3  8707  fpwwe2lem13  9032  tskuni  9173  recextlem2  10192  hashprg  12440  eqsqrt2d  13181  gcd1  14046  gcdeq  14066  phimullem  14185  pcgcd1  14276  pc2dvds  14278  pockthlem  14299  ablfacrplem  16988  lbsextlem4  17678  znrrg  18473  obslbs  18630  opnfbas  20211  supfil  20264  itg1addlem4  21974  itg1addlem5  21975  dvdsmulf1o  23336  ppiub  23345  dchrelbas4  23384  lgsne0  23474  2sqlem8  23513  tgldimor  23759  nbcusgra  24277  uvtxnbgra  24307  wlkcpr  24343  vdgr1b  24718  frgraunss  24809  qqhval2  27779  derangsn  28430  subfacp1lem6  28445  cvmsss2  28535  fperdvper  31562  wallispi  31684  fourierdlem56  31777  ax6e2ndeq  32768
  Copyright terms: Public domain W3C validator