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 2867
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 235 . 2 (𝐴 = 𝐵 → (𝜑𝜓))
4 pm2.61ne.2 . . 3 ((𝜑𝐴𝐵) → 𝜓)
54expcom 450 . 2 (𝐴𝐵 → (𝜑𝜓))
63, 5pm2.61ine 2865 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wne 2780
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 196  df-an 385  df-ne 2782
This theorem is referenced by:  pwdom  7997  cantnfle  8451  cantnflem1  8469  cantnf  8473  cdalepw  8901  infmap2  8923  zornn0g  9210  ttukeylem6  9219  msqge0  10428  xrsupsslem  12009  xrinfmsslem  12010  fzoss1  12364  swrdcl  13271  abs1m  13923  fsumcvg3  14307  bezoutlem4  15097  gcdmultiplez  15108  dvdssq  15118  lcmid  15160  pcdvdsb  15411  pcgcd1  15419  pc2dvds  15421  pcaddlem  15430  qexpz  15443  4sqlem19  15505  prmlem1a  15651  gsumwsubmcl  17198  gsumccat  17201  gsumwmhm  17205  zringlpir  19656  mretopd  20706  ufildom1  21540  alexsublem  21658  nmolb2d  22332  nmoi  22342  nmoix  22343  ipcau2  22841  mdegcl  23633  ply1divex  23700  ig1pcl  23739  dgrmulc  23831  mulcxplem  24230  vmacl  24644  efvmacl  24646  vmalelog  24730  padicabv  25119  nmlnoubi  27035  nmblolbii  27038  blocnilem  27043  blocni  27044  ubthlem1  27110  nmbdoplbi  28267  cnlnadjlem7  28316  branmfn  28348  pjbdlni  28392  shatomistici  28604  segcon2  31382  lssats  33317  ps-1  33781  3atlem5  33791  lplnnle2at  33845  2llnm3N  33873  lvolnle3at  33886  4atex2  34381  cdlemd5  34507  cdleme21k  34644  cdlemg33b  35013  mapdrvallem2  35952  mapdhcl  36034  hdmapval3N  36148  hdmap10  36150  hdmaprnlem17N  36173  hdmap14lem2a  36177  hdmaplkr  36223  hgmapvv  36236  cntzsdrg  36791  pfxcl  40249
  Copyright terms: Public domain W3C validator