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

Theorem pm2.61ne 3102
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
Hypotheses
Ref Expression
pm2.61ne.1 (𝐴 = 𝐵 → (𝜓𝜒))
pm2.61ne.2 ((𝜑𝐴𝐵) → 𝜓)
pm2.61ne.3 (𝜑𝜒)
Assertion
Ref Expression
pm2.61ne (𝜑𝜓)

Proof of Theorem pm2.61ne
StepHypRef Expression
1 pm2.61ne.3 . . 3 (𝜑𝜒)
2 pm2.61ne.1 . . 3 (𝐴 = 𝐵 → (𝜓𝜒))
31, 2syl5ibr 247 . 2 (𝐴 = 𝐵 → (𝜑𝜓))
4 pm2.61ne.2 . . 3 ((𝜑𝐴𝐵) → 𝜓)
54expcom 414 . 2 (𝐴𝐵 → (𝜑𝜓))
63, 5pm2.61ine 3100 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wne 3016
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 208  df-an 397  df-ne 3017
This theorem is referenced by:  pwdom  8658  cantnfle  9123  cantnflem1  9141  cantnf  9145  djulepw  9607  infmap2  9629  zornn0g  9916  ttukeylem6  9925  msqge0  11150  xrsupsslem  12690  xrinfmsslem  12691  fzoss1  13054  swrdcl  13997  pfxcl  14029  abs1m  14685  fsumcvg3  15076  bezoutlem4  15880  gcdmultiplezOLD  15891  dvdssq  15901  lcmid  15943  pcdvdsb  16195  pcgcd1  16203  pc2dvds  16205  pcaddlem  16214  qexpz  16227  4sqlem19  16289  prmlem1a  16430  gsumwsubmcl  17991  gsumccatOLD  17995  gsumccat  17996  gsumwmhm  18000  cntzsdrg  19512  zringlpir  20566  mretopd  21630  ufildom1  22464  alexsublem  22582  nmolb2d  23256  nmoi  23266  nmoix  23267  ipcau2  23766  mdegcl  24592  ply1divex  24659  ig1pcl  24698  dgrmulc  24790  mulcxplem  25194  vmacl  25623  efvmacl  25625  vmalelog  25709  padicabv  26134  nmlnoubi  28501  nmblolbii  28504  blocnilem  28509  blocni  28510  ubthlem1  28575  nmbdoplbi  29729  cnlnadjlem7  29778  branmfn  29810  pjbdlni  29854  shatomistici  30066  segcon2  33464  lssats  36030  ps-1  36495  3atlem5  36505  lplnnle2at  36559  2llnm3N  36587  lvolnle3at  36600  4atex2  37095  cdlemd5  37220  cdleme21k  37356  cdlemg33b  37725  mapdrvallem2  38663  mapdhcl  38745  hdmapval3N  38856  hdmap10  38858  hdmaprnlem17N  38881  hdmap14lem2a  38885  hdmaplkr  38931  hgmapvv  38944
  Copyright terms: Public domain W3C validator