Theorem necon3bd 2808

Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypothesis

Ref	Expression
necon3bd.1	|- ( ph -> ( A = B -> ps ) )

Assertion

Ref	Expression
necon3bd	|- ( ph -> ( -. ps -> A =/= B ) )

Proof of Theorem necon3bd

Step	Hyp	Ref	Expression
1		nne 2798	. . 3 |- ( -. A =/= B <-> A = B )
2		necon3bd.1	. . 3 |- ( ph -> ( A = B -> ps ) )
3	1, 2	syl5bi 232	. 2 |- ( ph -> ( -. A =/= B -> ps ) )
4	3	con1d 139	1 |- ( ph -> ( -. ps -> A =/= B ) )

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:  necon2ad  2809  nelne1  2890  nelne2  2891  nssne1  3661  nssne2  3662  disjne  4022  nbrne1  4672  nbrne2  4673  peano5  7089  oeeui  7682  domdifsn  8043  ac6sfi  8204  inf3lem2  8526  cnfcom3lem  8600  dfac9  8958  fin23lem21  9161  dedekindle  10201  zneo  11460  modirr  12741  sqrmo  13992  pc2dvds  15583  pcadd  15593  oddprmdvds  15607  4sqlem11  15659  latnlej  17068  sylow2blem3  18037  irredn0  18703  irredn1  18706  lssneln0  18952  lspsnne2  19118  lspfixed  19128  lspindpi  19132  lsmcv  19141  lspsolv  19143  isnzr2  19263  coe1tmmul  19647  dfac14  21421  fbdmn0  21638  filufint  21724  flimfnfcls  21832  alexsubALTlem2  21852  evth  22758  cphsqrtcl2  22986  ovolicc2lem4  23288  lhop1lem  23776  lhop1  23777  lhop2  23778  lhop  23779  deg1add  23863  abelthlem2  24186  logcnlem2  24389  angpined  24557  asinneg  24613  dmgmaddn0  24749  lgsne0  25060  lgsqr  25076  lgsquadlem2  25106  lgsquadlem3  25107  axlowdimlem17  25838  spansncvi  28511  broutsideof2  32229  unblimceq0lem  32497  poimirlem28  33437  dvasin  33496  dvacos  33497  nninfnub  33547  dvrunz  33753  lsatcvatlem  34336  lkrlsp2  34390  opnlen0  34475  2llnne2N  34694  lnnat  34713  llnn0  34802  lplnn0N  34833  lplnllnneN  34842  llncvrlpln2  34843  llncvrlpln  34844  lvoln0N  34877  lplncvrlvol2  34901  lplncvrlvol  34902  dalempnes  34937  dalemqnet  34938  dalemcea  34946  dalem3  34950  cdlema1N  35077  cdlemb  35080  paddasslem5  35110  llnexchb2lem  35154  osumcllem4N  35245  pexmidlem1N  35256  lhp2lt  35287  lhp2atne  35320  lhp2at0ne  35322  4atexlemunv  35352  4atexlemex2  35357  trlne  35472  trlval4  35475  cdlemc4  35481  cdleme11dN  35549  cdleme11h  35553  cdlemednuN  35587  cdleme20j  35606  cdleme20k  35607  cdleme21at  35616  cdleme35f  35742  cdlemg11b  35930  dia2dimlem1  36353  dihmeetlem3N  36594  dihmeetlem15N  36610  dochsnnz  36739  dochexmidlem1  36749  dochexmidlem7  36755  mapdindp3  37011  pellexlem1  37393  dfac21  37636  pm13.14  38610  uzlidlring  41929  suppdm  42300