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 3056
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 238 . 2 (𝐴 = 𝐵 → (𝜑𝜓))
4 pm2.61ne.2 . . 3 ((𝜑𝐴𝐵) → 𝜓)
54expcom 403 . 2 (𝐴𝐵 → (𝜑𝜓))
63, 5pm2.61ine 3054 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385   = wceq 1653  wne 2971
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 199  df-an 386  df-ne 2972
This theorem is referenced by:  pwdom  8354  cantnfle  8818  cantnflem1  8836  cantnf  8840  cdalepw  9306  infmap2  9328  zornn0g  9615  ttukeylem6  9624  msqge0  10841  xrsupsslem  12386  xrinfmsslem  12387  fzoss1  12750  swrdcl  13669  pfxcl  13720  abs1m  14416  fsumcvg3  14801  bezoutlem4  15594  gcdmultiplez  15605  dvdssq  15615  lcmid  15657  pcdvdsb  15906  pcgcd1  15914  pc2dvds  15916  pcaddlem  15925  qexpz  15938  4sqlem19  16000  prmlem1a  16141  gsumwsubmcl  17690  gsumccat  17693  gsumwmhm  17698  zringlpir  20159  mretopd  21225  ufildom1  22058  alexsublem  22176  nmolb2d  22850  nmoi  22860  nmoix  22861  ipcau2  23360  mdegcl  24170  ply1divex  24237  ig1pcl  24276  dgrmulc  24368  mulcxplem  24771  vmacl  25196  efvmacl  25198  vmalelog  25282  padicabv  25671  nmlnoubi  28176  nmblolbii  28179  blocnilem  28184  blocni  28185  ubthlem1  28251  nmbdoplbi  29408  cnlnadjlem7  29457  branmfn  29489  pjbdlni  29533  shatomistici  29745  segcon2  32725  lssats  35033  ps-1  35498  3atlem5  35508  lplnnle2at  35562  2llnm3N  35590  lvolnle3at  35603  4atex2  36098  cdlemd5  36223  cdleme21k  36359  cdlemg33b  36728  mapdrvallem2  37666  mapdhcl  37748  hdmapval3N  37859  hdmap10  37861  hdmaprnlem17N  37884  hdmap14lem2a  37888  hdmaplkr  37934  hgmapvv  37947  cntzsdrg  38557
  Copyright terms: Public domain W3C validator