Theorem necon3ad 2635

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 23	. . 3 |- ( A =/= B -> A =/= B )
3	2	neneqd 2626	. 2 |- ( A =/= B -> -. A = B )
4	1, 3	nsyli 147	1 |- ( ph -> ( A =/= B -> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1438   =/= wne 2619

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 189  df-ne 2621

This theorem is referenced by:  necon1ad  2641  necon3d  2649  disjpss  3844  oeeulem  7308  enp1i  7810  canthp1lem2  9080  winalim2  9123  nlt1pi  9333  sqreulem  13416  rpnnen2lem11  14270  dvdseq  14345  eucalglt  14537  nprm  14631  pcprmpw2  14824  pcmpt  14830  expnprm  14840  prmlem0  15070  pltnle  16205  psgnunilem1  17127  pgpfi  17250  frgpnabllem1  17502  gsumval3a  17530  ablfac1eulem  17698  pgpfaclem2  17708  lspdisjb  18342  lspdisj2  18343  obselocv  19283  0nnei  20120  t0dist  20333  t1sep  20378  ordthauslem  20391  hausflim  20988  bcthlem5  22288  bcth  22289  fta1g  23110  plyco0  23138  dgrnznn  23193  coeaddlem  23195  fta1  23253  vieta1lem2  23256  logcnlem3  23581  dvloglem  23585  dcubic  23764  mumullem2  24099  2sqlem8a  24291  dchrisum0flblem1  24338  colperpexlem2  24765  ocnel  26943  hatomistici  28007  sibfof  29175  outsideofrflx  30893  poimirlem23  31921  mblfinlem1  31935  cntotbnd  32086  heiborlem6  32106  lshpnel  32512  lshpcmp  32517  lfl1  32599  lkrshp  32634  lkrpssN  32692  atnlt  32842  atnle  32846  atlatmstc  32848  intnatN  32935  atbtwn  32974  llnnlt  33051  lplnnlt  33093  2llnjaN  33094  lvolnltN  33146  2lplnja  33147  dalem-cly  33199  dalem44  33244  2llnma3r  33316  cdlemblem  33321  lhpm0atN  33557  lhp2atnle  33561  cdlemednpq  33828  cdleme22cN  33872  cdlemg18b  34209  cdlemg42  34259  dia2dimlem1  34595  dochkrshp  34917  hgmapval0  35426  2f1fvneq  38757