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

Theorem necon3ad 2836
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 2829 . 2 (𝐴𝐵 → ¬ 𝐴 = 𝐵)
31, 2nsyli 155 1 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 2824
This theorem is referenced by:  necon1ad  2840  necon3d  2844  disjpss  4061  2f1fvneq  6557  oeeulem  7726  enp1i  8236  canthp1lem2  9513  winalim2  9556  nlt1pi  9766  sqreulem  14143  rpnnen2lem11  14997  eucalglt  15345  nprm  15448  pcprmpw2  15633  pcmpt  15643  expnprm  15653  prmlem0  15859  pltnle  17013  psgnunilem1  17959  pgpfi  18066  frgpnabllem1  18322  gsumval3a  18350  ablfac1eulem  18517  pgpfaclem2  18527  lspdisjb  19174  lspdisj2  19175  obselocv  20120  0nnei  20964  t0dist  21177  t1sep  21222  ordthauslem  21235  hausflim  21832  bcthlem5  23171  bcth  23172  fta1g  23972  plyco0  23993  dgrnznn  24048  coeaddlem  24050  fta1  24108  vieta1lem2  24111  logcnlem3  24435  dvloglem  24439  dcubic  24618  mumullem2  24951  2sqlem8a  25195  dchrisum0flblem1  25242  colperpexlem2  25668  1loopgrnb0  26454  usgr2trlncrct  26754  ocnel  28285  hatomistici  29349  sibfof  30530  outsideofrflx  32359  poimirlem23  33562  mblfinlem1  33576  cntotbnd  33725  heiborlem6  33745  lshpnel  34588  lshpcmp  34593  lfl1  34675  lkrshp  34710  lkrpssN  34768  atnlt  34918  atnle  34922  atlatmstc  34924  intnatN  35011  atbtwn  35050  llnnlt  35127  lplnnlt  35169  2llnjaN  35170  lvolnltN  35222  2lplnja  35223  dalem-cly  35275  dalem44  35320  2llnma3r  35392  cdlemblem  35397  lhpm0atN  35633  lhp2atnle  35637  cdlemednpq  35904  cdleme22cN  35947  cdlemg18b  36284  cdlemg42  36334  dia2dimlem1  36670  dochkrshp  36992  hgmapval0  37501
  Copyright terms: Public domain W3C validator