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 3027
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, 2imbitrrid 245 . 2 (𝐴 = 𝐵 → (𝜑𝜓))
4 pm2.61ne.2 . . 3 ((𝜑𝐴𝐵) → 𝜓)
54expcom 415 . 2 (𝐴𝐵 → (𝜑𝜓))
63, 5pm2.61ine 3025 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wne 2940
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 206  df-an 398  df-ne 2941
This theorem is referenced by:  pwdom  9076  cantnfle  9612  cantnflem1  9630  cantnf  9634  djulepw  10133  infmap2  10159  zornn0g  10446  ttukeylem6  10455  msqge0  11681  xrsupsslem  13232  xrinfmsslem  13233  fzoss1  13605  swrdcl  14539  pfxcl  14571  abs1m  15226  fsumcvg3  15619  bezoutlem4  16428  dvdssq  16448  lcmid  16490  pcdvdsb  16746  pcgcd1  16754  pc2dvds  16756  pcaddlem  16765  qexpz  16778  4sqlem19  16840  prmlem1a  16984  gsumwsubmcl  18652  gsumccat  18656  gsumwmhm  18660  cntzsdrg  20283  zringlpir  20904  mretopd  22459  ufildom1  23293  alexsublem  23411  nmolb2d  24098  nmoi  24108  nmoix  24109  ipcau2  24614  mdegcl  25450  ply1divex  25517  ig1pcl  25556  dgrmulc  25648  mulcxplem  26055  vmacl  26483  efvmacl  26485  vmalelog  26569  padicabv  26994  nmlnoubi  29780  nmblolbii  29783  blocnilem  29788  blocni  29789  ubthlem1  29854  nmbdoplbi  31008  cnlnadjlem7  31057  branmfn  31089  pjbdlni  31133  shatomistici  31345  segcon2  34736  lssats  37520  ps-1  37986  3atlem5  37996  lplnnle2at  38050  2llnm3N  38078  lvolnle3at  38091  4atex2  38586  cdlemd5  38711  cdleme21k  38847  cdlemg33b  39216  mapdrvallem2  40154  mapdhcl  40236  hdmapval3N  40347  hdmap10  40349  hdmaprnlem17N  40372  hdmap14lem2a  40376  hdmaplkr  40422  hgmapvv  40435
  Copyright terms: Public domain W3C validator