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

Theorem necon3ad 3020
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 3013 . 2 (𝐴𝐵 → ¬ 𝐴 = 𝐵)
31, 2nsyli 160 1 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  wne 3007
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 210  df-ne 3008
This theorem is referenced by:  necon1ad  3024  necon3d  3028  disjpss  4383  2f1fvneq  6992  oeeulem  8202  enp1i  8729  canthp1lem2  10052  winalim2  10095  nlt1pi  10305  sqreulem  14698  rpnnen2lem11  15556  eucalglt  15906  nprm  16009  pcprmpw2  16195  pcmpt  16205  expnprm  16215  prmlem0  16417  pltnle  17554  psgnunilem1  18599  pgpfi  18708  frgpnabllem1  18971  gsumval3a  19001  ablfac1eulem  19172  pgpfaclem2  19182  ablsimpgfindlem1  19207  lspdisjb  19873  lspdisj2  19874  obselocv  20847  0nnei  21695  t0dist  21908  t1sep  21953  ordthauslem  21966  hausflim  22564  bcthlem5  23910  bcth  23911  fta1g  24746  plyco0  24767  dgrnznn  24822  coeaddlem  24824  fta1  24882  vieta1lem2  24885  logcnlem3  25213  dvloglem  25217  dcubic  25410  mumullem2  25743  2sqlem8a  25987  dchrisum0flblem1  26070  colperpexlem2  26503  elntg2  26757  1loopgrnb0  27270  usgr2trlncrct  27570  ocnel  29059  hatomistici  30123  lbslsat  31024  sibfof  31605  outsideofrflx  33595  poimirlem23  34960  mblfinlem1  34974  cntotbnd  35114  heiborlem6  35134  lshpnel  36159  lshpcmp  36164  lfl1  36246  lkrshp  36281  lkrpssN  36339  atnlt  36489  atnle  36493  atlatmstc  36495  intnatN  36583  atbtwn  36622  llnnlt  36699  lplnnlt  36741  2llnjaN  36742  lvolnltN  36794  2lplnja  36795  dalem-cly  36847  dalem44  36892  2llnma3r  36964  cdlemblem  36969  lhpm0atN  37205  lhp2atnle  37209  cdlemednpq  37475  cdleme22cN  37518  cdlemg18b  37855  cdlemg42  37905  dia2dimlem1  38240  dochkrshp  38562  hgmapval0  39068  rrx2pnecoorneor  44891
  Copyright terms: Public domain W3C validator