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

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

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