Theorem necon3ad 2677

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

Hypothesis

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

Assertion

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

Proof of Theorem necon3ad

Step	Hyp	Ref	Expression
1		necon3ad.1	. 2 |- ( ph -> ( ps -> A = B ) )
2		id 22	. . 3 |- ( A =/= B -> A =/= B )
3	2	neneqd 2669	. 2 |- ( A =/= B -> -. A = B )
4	1, 3	nsyli 141	1 |- ( ph -> ( A =/= B -> -. ps ) )

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:  necon1ad  2683  necon3d  2691  disjpss  3877  oeeulem  7247  enp1i  7751  canthp1lem2  9027  winalim2  9070  nlt1pi  9280  sqreulem  13151  rpnnen2lem11  13815  dvdseq  13888  eucalglt  14069  nprm  14086  pcprmpw2  14260  pcmpt  14266  expnprm  14276  prmlem0  14445  pltnle  15449  psgnunilem1  16314  pgpfi  16421  frgpnabllem1  16668  gsumval3a  16696  gsumval3aOLD  16697  ablfac1eulem  16913  pgpfaclem2  16923  lspdisjb  17555  lspdisj2  17556  obselocv  18526  0nnei  19379  t0dist  19592  t1sep  19637  ordthauslem  19650  hausflim  20217  bcthlem5  21502  bcth  21503  fta1g  22303  plyco0  22324  coeaddlem  22380  fta1  22438  vieta1lem2  22441  logcnlem3  22753  dvloglem  22757  dcubic  22905  mumullem2  23182  2sqlem8a  23374  dchrisum0flblem1  23421  colperpexlem2  23810  ocnel  25892  hatomistici  26957  sibfof  27922  outsideofrflx  29354  mblfinlem1  29628  cntotbnd  29895  heiborlem6  29915  dgrnznn  30689  2f1fvneq  31776  lshpnel  33780  lshpcmp  33785  lfl1  33867  lkrshp  33902  lkrpssN  33960  atnlt  34110  atnle  34114  atlatmstc  34116  intnatN  34203  atbtwn  34242  llnnlt  34319  lplnnlt  34361  2llnjaN  34362  lvolnltN  34414  2lplnja  34415  dalem-cly  34467  dalem44  34512  2llnma3r  34584  cdlemblem  34589  lhpm0atN  34825  lhp2atnle  34829  cdlemednpq  35095  cdleme22cN  35138  cdlemg18b  35475  cdlemg42  35525  dia2dimlem1  35861  dochkrshp  36183  hgmapval0  36692