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

Step	Hyp	Ref	Expression
1		necon3ai.1	. . 3 |- ( ph -> A = B )
2		nne 2655	. . 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 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