Theorem necon3ad 2639

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1446   =/= wne 2624

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 2626

This theorem is referenced by:  necon1ad  2643  necon3d  2647  disjpss  3817  oeeulem  7307  enp1i  7811  canthp1lem2  9083  winalim2  9126  nlt1pi  9336  sqreulem  13434  rpnnen2lem11  14289  dvdseq  14364  eucalglt  14556  nprm  14650  pcprmpw2  14843  pcmpt  14849  expnprm  14859  prmlem0  15089  pltnle  16224  psgnunilem1  17146  pgpfi  17269  frgpnabllem1  17521  gsumval3a  17549  ablfac1eulem  17717  pgpfaclem2  17727  lspdisjb  18361  lspdisj2  18362  obselocv  19303  0nnei  20140  t0dist  20353  t1sep  20398  ordthauslem  20411  hausflim  21008  bcthlem5  22308  bcth  22309  fta1g  23130  plyco0  23158  dgrnznn  23213  coeaddlem  23215  fta1  23273  vieta1lem2  23276  logcnlem3  23601  dvloglem  23605  dcubic  23784  mumullem2  24119  2sqlem8a  24311  dchrisum0flblem1  24358  colperpexlem2  24785  ocnel  26963  hatomistici  28027  sibfof  29185  outsideofrflx  30906  poimirlem23  31975  mblfinlem1  31989  cntotbnd  32140  heiborlem6  32160  lshpnel  32561  lshpcmp  32566  lfl1  32648  lkrshp  32683  lkrpssN  32741  atnlt  32891  atnle  32895  atlatmstc  32897  intnatN  32984  atbtwn  33023  llnnlt  33100  lplnnlt  33142  2llnjaN  33143  lvolnltN  33195  2lplnja  33196  dalem-cly  33248  dalem44  33293  2llnma3r  33365  cdlemblem  33370  lhpm0atN  33606  lhp2atnle  33610  cdlemednpq  33877  cdleme22cN  33921  cdlemg18b  34258  cdlemg42  34308  dia2dimlem1  34644  dochkrshp  34966  hgmapval0  35475  2f1fvneq  39024  uspgrloopnb0  39566