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

Theorem necon3ad 2794
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 2787 . 2 (𝐴𝐵 → ¬ 𝐴 = 𝐵)
31, 2nsyli 153 1 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wne 2779
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 195  df-ne 2781
This theorem is referenced by:  necon1ad  2798  necon3d  2802  disjpss  3979  oeeulem  7545  enp1i  8057  canthp1lem2  9331  winalim2  9374  nlt1pi  9584  sqreulem  13893  rpnnen2lem11  14738  eucalglt  15082  nprm  15185  pcprmpw2  15370  pcmpt  15380  expnprm  15390  prmlem0  15596  pltnle  16735  psgnunilem1  17682  pgpfi  17789  frgpnabllem1  18045  gsumval3a  18073  ablfac1eulem  18240  pgpfaclem2  18250  lspdisjb  18893  lspdisj2  18894  obselocv  19833  0nnei  20668  t0dist  20881  t1sep  20926  ordthauslem  20939  hausflim  21537  bcthlem5  22850  bcth  22851  fta1g  23648  plyco0  23669  dgrnznn  23724  coeaddlem  23726  fta1  23784  vieta1lem2  23787  logcnlem3  24107  dvloglem  24111  dcubic  24290  mumullem2  24623  2sqlem8a  24867  dchrisum0flblem1  24914  colperpexlem2  25341  ocnel  27347  hatomistici  28411  sibfof  29535  outsideofrflx  31210  poimirlem23  32398  mblfinlem1  32412  cntotbnd  32561  heiborlem6  32581  lshpnel  33084  lshpcmp  33089  lfl1  33171  lkrshp  33206  lkrpssN  33264  atnlt  33414  atnle  33418  atlatmstc  33420  intnatN  33507  atbtwn  33546  llnnlt  33623  lplnnlt  33665  2llnjaN  33666  lvolnltN  33718  2lplnja  33719  dalem-cly  33771  dalem44  33816  2llnma3r  33888  cdlemblem  33893  lhpm0atN  34129  lhp2atnle  34133  cdlemednpq  34400  cdleme22cN  34444  cdlemg18b  34781  cdlemg42  34831  dia2dimlem1  35167  dochkrshp  35489  hgmapval0  35998  2f1fvneq  40131  1loopgrnb0  40712  usgr2trlncrct  41004
  Copyright terms: Public domain W3C validator