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 2861
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 234 . 2 (𝐴 = 𝐵 → (𝜑𝜓))
4 pm2.61ne.2 . . 3 ((𝜑𝐴𝐵) → 𝜓)
54expcom 449 . 2 (𝐴𝐵 → (𝜑𝜓))
63, 5pm2.61ine 2859 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wne 2774
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-an 384  df-ne 2776
This theorem is referenced by:  pwdom  7969  cantnfle  8423  cantnflem1  8441  cantnf  8445  cdalepw  8873  infmap2  8895  zornn0g  9182  ttukeylem6  9191  msqge0  10393  xrsupsslem  11960  xrinfmsslem  11961  fzoss1  12314  swrdcl  13212  abs1m  13864  fsumcvg3  14248  bezoutlem4  15038  gcdmultiplez  15049  dvdssq  15059  lcmid  15101  pcdvdsb  15352  pcgcd1  15360  pc2dvds  15362  pcaddlem  15371  qexpz  15384  4sqlem19  15446  prmlem1a  15592  gsumwsubmcl  17139  gsumccat  17142  gsumwmhm  17146  zringlpir  19595  mretopd  20643  ufildom1  21477  alexsublem  21595  nmolb2d  22259  nmoi  22269  nmoix  22270  ipcau2  22757  mdegcl  23545  ply1divex  23612  ig1pcl  23651  dgrmulc  23743  mulcxplem  24142  vmacl  24556  efvmacl  24558  vmalelog  24642  padicabv  25031  nmlnoubi  26836  nmblolbii  26839  blocnilem  26844  blocni  26845  ubthlem1  26911  nmbdoplbi  28068  cnlnadjlem7  28117  branmfn  28149  pjbdlni  28193  shatomistici  28405  segcon2  31183  lssats  33115  ps-1  33579  3atlem5  33589  lplnnle2at  33643  2llnm3N  33671  lvolnle3at  33684  4atex2  34179  cdlemd5  34305  cdleme21k  34442  cdlemg33b  34811  mapdrvallem2  35750  mapdhcl  35832  hdmapval3N  35946  hdmap10  35948  hdmaprnlem17N  35971  hdmap14lem2a  35975  hdmaplkr  36021  hgmapvv  36034  cntzsdrg  36589  pfxcl  40049
  Copyright terms: Public domain W3C validator