Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon3ad Structured version   Visualization version   GIF version

 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 (𝜑 → (𝜓𝐴 = 𝐵))
Assertion
Ref Expression
necon3ad (𝜑 → (𝐴𝐵 → ¬ 𝜓))

Proof of Theorem necon3ad
StepHypRef Expression
1 necon3ad.1 . 2 (𝜑 → (𝜓𝐴 = 𝐵))
2 neneq 2938 . 2 (𝐴𝐵 → ¬ 𝐴 = 𝐵)
31, 2nsyli 155 1 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1632   ≠ wne 2932 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 2933 This theorem is referenced by:  necon1ad  2949  necon3d  2953  disjpss  4172  2f1fvneq  6680  oeeulem  7850  enp1i  8360  canthp1lem2  9667  winalim2  9710  nlt1pi  9920  sqreulem  14298  rpnnen2lem11  15152  eucalglt  15500  nprm  15603  pcprmpw2  15788  pcmpt  15798  expnprm  15808  prmlem0  16014  pltnle  17167  psgnunilem1  18113  pgpfi  18220  frgpnabllem1  18476  gsumval3a  18504  ablfac1eulem  18671  pgpfaclem2  18681  lspdisjb  19328  lspdisj2  19329  obselocv  20274  0nnei  21118  t0dist  21331  t1sep  21376  ordthauslem  21389  hausflim  21986  bcthlem5  23325  bcth  23326  fta1g  24126  plyco0  24147  dgrnznn  24202  coeaddlem  24204  fta1  24262  vieta1lem2  24265  logcnlem3  24589  dvloglem  24593  dcubic  24772  mumullem2  25105  2sqlem8a  25349  dchrisum0flblem1  25396  colperpexlem2  25822  1loopgrnb0  26608  usgr2trlncrct  26909  ocnel  28466  hatomistici  29530  sibfof  30711  outsideofrflx  32540  poimirlem23  33745  mblfinlem1  33759  cntotbnd  33908  heiborlem6  33928  lshpnel  34773  lshpcmp  34778  lfl1  34860  lkrshp  34895  lkrpssN  34953  atnlt  35103  atnle  35107  atlatmstc  35109  intnatN  35196  atbtwn  35235  llnnlt  35312  lplnnlt  35354  2llnjaN  35355  lvolnltN  35407  2lplnja  35408  dalem-cly  35460  dalem44  35505  2llnma3r  35577  cdlemblem  35582  lhpm0atN  35818  lhp2atnle  35822  cdlemednpq  36089  cdleme22cN  36132  cdlemg18b  36469  cdlemg42  36519  dia2dimlem1  36855  dochkrshp  37177  hgmapval0  37686
 Copyright terms: Public domain W3C validator