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 2876
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 236 . 2 (𝐴 = 𝐵 → (𝜑𝜓))
4 pm2.61ne.2 . . 3 ((𝜑𝐴𝐵) → 𝜓)
54expcom 451 . 2 (𝐴𝐵 → (𝜑𝜓))
63, 5pm2.61ine 2874 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wne 2791
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-an 386  df-ne 2792
This theorem is referenced by:  pwdom  8097  cantnfle  8553  cantnflem1  8571  cantnf  8575  cdalepw  9003  infmap2  9025  zornn0g  9312  ttukeylem6  9321  msqge0  10534  xrsupsslem  12122  xrinfmsslem  12123  fzoss1  12479  swrdcl  13401  abs1m  14056  fsumcvg3  14441  bezoutlem4  15240  gcdmultiplez  15251  dvdssq  15261  lcmid  15303  pcdvdsb  15554  pcgcd1  15562  pc2dvds  15564  pcaddlem  15573  qexpz  15586  4sqlem19  15648  prmlem1a  15794  gsumwsubmcl  17356  gsumccat  17359  gsumwmhm  17363  zringlpir  19818  mretopd  20877  ufildom1  21711  alexsublem  21829  nmolb2d  22503  nmoi  22513  nmoix  22514  ipcau2  23014  mdegcl  23810  ply1divex  23877  ig1pcl  23916  dgrmulc  24008  mulcxplem  24411  vmacl  24825  efvmacl  24827  vmalelog  24911  padicabv  25300  nmlnoubi  27621  nmblolbii  27624  blocnilem  27629  blocni  27630  ubthlem1  27696  nmbdoplbi  28853  cnlnadjlem7  28902  branmfn  28934  pjbdlni  28978  shatomistici  29190  segcon2  32187  lssats  34118  ps-1  34582  3atlem5  34592  lplnnle2at  34646  2llnm3N  34674  lvolnle3at  34687  4atex2  35182  cdlemd5  35308  cdleme21k  35445  cdlemg33b  35814  mapdrvallem2  36753  mapdhcl  36835  hdmapval3N  36949  hdmap10  36951  hdmaprnlem17N  36974  hdmap14lem2a  36978  hdmaplkr  37024  hgmapvv  37037  cntzsdrg  37591  pfxcl  41151
  Copyright terms: Public domain W3C validator