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

Theorem pm2.61ne 3100
 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 248 . 2 (𝐴 = 𝐵 → (𝜑𝜓))
4 pm2.61ne.2 . . 3 ((𝜑𝐴𝐵) → 𝜓)
54expcom 416 . 2 (𝐴𝐵 → (𝜑𝜓))
63, 5pm2.61ine 3098 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1531   ≠ wne 3014 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 209  df-an 399  df-ne 3015 This theorem is referenced by:  pwdom  8661  cantnfle  9126  cantnflem1  9144  cantnf  9148  djulepw  9610  infmap2  9632  zornn0g  9919  ttukeylem6  9928  msqge0  11153  xrsupsslem  12692  xrinfmsslem  12693  fzoss1  13056  swrdcl  13999  pfxcl  14031  abs1m  14687  fsumcvg3  15078  bezoutlem4  15882  gcdmultiplezOLD  15893  dvdssq  15903  lcmid  15945  pcdvdsb  16197  pcgcd1  16205  pc2dvds  16207  pcaddlem  16216  qexpz  16229  4sqlem19  16291  prmlem1a  16432  gsumwsubmcl  17993  gsumccatOLD  17997  gsumccat  17998  gsumwmhm  18002  cntzsdrg  19573  zringlpir  20628  mretopd  21692  ufildom1  22526  alexsublem  22644  nmolb2d  23319  nmoi  23329  nmoix  23330  ipcau2  23829  mdegcl  24655  ply1divex  24722  ig1pcl  24761  dgrmulc  24853  mulcxplem  25259  vmacl  25687  efvmacl  25689  vmalelog  25773  padicabv  26198  nmlnoubi  28565  nmblolbii  28568  blocnilem  28573  blocni  28574  ubthlem1  28639  nmbdoplbi  29793  cnlnadjlem7  29842  branmfn  29874  pjbdlni  29918  shatomistici  30130  segcon2  33559  lssats  36140  ps-1  36605  3atlem5  36615  lplnnle2at  36669  2llnm3N  36697  lvolnle3at  36710  4atex2  37205  cdlemd5  37330  cdleme21k  37466  cdlemg33b  37835  mapdrvallem2  38773  mapdhcl  38855  hdmapval3N  38966  hdmap10  38968  hdmaprnlem17N  38991  hdmap14lem2a  38995  hdmaplkr  39041  hgmapvv  39054
 Copyright terms: Public domain W3C validator