Theorem necon3ai 2819

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 2798	. . 3 |- ( -. A =/= B <-> A = B )
3	1, 2	sylibr 224	. 2 |- ( ph -> -. A =/= B )
4	3	con2i 134	1 |- ( A =/= B -> -. ph )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

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 197  df-ne 2795

This theorem is referenced by:  necon1ai  2821  necon3i  2826  neneor  2893  nelsn  4212  disjsn2  4247  opelopabsb  4985  0nelxpOLD  5144  funsndifnop  6416  map0b  7896  mapdom3  8132  wemapso2lem  8457  cflim2  9085  isfin4-3  9137  fpwwe2lem13  9464  tskuni  9605  recextlem2  10658  hashprg  13182  hashprgOLD  13183  eqsqrt2d  14108  gcd1  15249  gcdzeq  15271  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  phimullem  15484  pcgcd1  15581  pc2dvds  15583  pockthlem  15609  ablfacrplem  18464  znrrg  19914  opnfbas  21646  supfil  21699  itg1addlem4  23466  itg1addlem5  23467  dvdsmulf1o  24920  ppiub  24929  dchrelbas4  24968  lgsne0  25060  2sqlem8  25151  tgldimor  25397  subfacp1lem6  31167  cvmsss2  31256  ax6e2ndeq  38775  supminfxr2  39699  fourierdlem56  40379