Theorem necon3ai 2649

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

Step	Hyp	Ref	Expression
1		necon3ai.1	. . 3 |- ( ph -> A = B )
2		nne 2628	. . 3 |- ( -. A =/= B <-> A = B )
3	1, 2	sylibr 217	. 2 |- ( ph -> -. A =/= B )
4	3	con2i 125	1 |- ( A =/= B -> -. ph )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1448   =/= wne 2622

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 190  df-ne 2624

This theorem is referenced by:  necon1ai  2651  necon3i  2656  neneor  2722  disjsn2  4001  opelopabsb  4684  0nelxp  4840  fvunsn  6081  map0b  7497  mapdom3  7731  wemapso2lem  8054  cflim2  8680  isfin4-3  8732  fpwwe2lem13  9054  tskuni  9195  recextlem2  10232  hashprg  12566  eqsqrt2d  13442  gcd1  14507  gcdeq  14531  lcmfunsnlem2lem1  14622  lcmfunsnlem2lem2  14623  phimullem  14738  pcgcd1  14837  pc2dvds  14839  pockthlem  14860  ablfacrplem  17709  lbsextlem4  18395  znrrg  19147  obslbs  19304  opnfbas  20868  supfil  20921  itg1addlem4  22669  itg1addlem5  22670  dvdsmulf1o  24135  ppiub  24144  dchrelbas4  24183  lgsne0  24273  2sqlem8  24312  tgldimor  24558  nbcusgra  25203  uvtxnbgra  25233  wlkcpr  25269  vdgr1b  25644  frgraunss  25735  submateqlem1  28640  submateqlem2  28641  qqhval2  28793  derangsn  29899  subfacp1lem6  29914  cvmsss2  30003  ax6e2ndeq  36927  fperdvper  37832  dvnmul  37860  wallispi  37989  fourierdlem56  38083  gcdzeq  38884  funsndifnop  39116