Theorem necon3ad 2658

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 2651	. 2 |- ( A =/= B -> -. A = B )
4	1, 3	nsyli 141	1 |- ( ph -> ( A =/= B -> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1370   =/= wne 2644

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 2646

This theorem is referenced by:  necon1ad  2664  necon3d  2672  disjpss  3830  oeeulem  7143  enp1i  7651  canthp1lem2  8924  winalim2  8967  nlt1pi  9179  sqreulem  12958  rpnnen2lem11  13618  dvdseq  13691  eucalglt  13871  nprm  13888  pcprmpw2  14059  pcmpt  14065  expnprm  14075  prmlem0  14244  pltnle  15247  psgnunilem1  16110  pgpfi  16217  frgpnabllem1  16464  gsumval3a  16492  gsumval3aOLD  16493  ablfac1eulem  16687  pgpfaclem2  16697  lspdisjb  17322  lspdisj2  17323  obselocv  18271  0nnei  18841  t0dist  19054  t1sep  19099  ordthauslem  19112  hausflim  19679  bcthlem5  20964  bcth  20965  fta1g  21765  plyco0  21786  coeaddlem  21842  fta1  21900  vieta1lem2  21903  logcnlem3  22215  dvloglem  22219  dcubic  22367  mumullem2  22644  2sqlem8a  22836  dchrisum0flblem1  22883  colperplem2  23251  ocnel  24846  hatomistici  25911  sibfof  26863  outsideofrflx  28295  mblfinlem1  28569  cntotbnd  28836  heiborlem6  28856  dgrnznn  29633  2f1fvneq  30284  lshpnel  32937  lshpcmp  32942  lfl1  33024  lkrshp  33059  lkrpssN  33117  atnlt  33267  atnle  33271  atlatmstc  33273  intnatN  33360  atbtwn  33399  llnnlt  33476  lplnnlt  33518  2llnjaN  33519  lvolnltN  33571  2lplnja  33572  dalem-cly  33624  dalem44  33669  2llnma3r  33741  cdlemblem  33746  lhpm0atN  33982  lhp2atnle  33986  cdlemednpq  34252  cdleme22cN  34295  cdlemg18b  34632  cdlemg42  34682  dia2dimlem1  35018  dochkrshp  35340  hgmapval0  35849