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

Theorem pm2.61dne 3028
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
pm2.61dne.1 (𝜑 → (𝐴 = 𝐵𝜓))
pm2.61dne.2 (𝜑 → (𝐴𝐵𝜓))
Assertion
Ref Expression
pm2.61dne (𝜑𝜓)

Proof of Theorem pm2.61dne
StepHypRef Expression
1 pm2.61dne.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
21com12 32 . 2 (𝐴 = 𝐵 → (𝜑𝜓))
3 pm2.61dne.2 . . 3 (𝜑 → (𝐴𝐵𝜓))
43com12 32 . 2 (𝐴𝐵 → (𝜑𝜓))
52, 4pm2.61ine 3025 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = 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-ne 2941
This theorem is referenced by:  pm2.61dane  3029  wefrc  5628  wereu2  5631  frpomin  6295  oe0lem  8460  fisupg  9238  marypha1lem  9374  fiinfg  9440  wdomtr  9516  unxpwdom2  9529  frmin  9690  fpwwe2lem12  10583  grur1a  10760  grutsk  10763  fimaxre2  12105  xlesubadd  13188  cshwidxmod  14697  sqreu  15251  pcxnn0cl  16737  pcxcl  16738  pcmpt  16769  symggen  19257  isabvd  20293  lspprat  20630  mdetralt  21973  ordtrest2lem  22570  ordthauslem  22750  comppfsc  22899  fbssint  23205  fclscf  23392  tgptsmscld  23518  ovoliunnul  24887  itg11  25071  i1fadd  25075  fta1g  25548  plydiveu  25674  fta1  25684  mulcxp  26056  cxpsqrt  26074  ostth3  27002  madebdaylemlrcut  27250  brbtwn2  27896  colinearalg  27901  clwwisshclwws  29001  ordtrest2NEWlem  32560  subfacp1lem5  33835  btwnexch2  34654  fnemeet2  34885  fnejoin2  34887  limsucncmpi  34963  areacirc  36217  sstotbnd2  36279  ssbnd  36293  prdsbnd2  36300  rrncmslem  36337  atnlt  37821  atlelt  37947  llnnlt  38032  lplnnlt  38074  lvolnltN  38127  pmapglb2N  38280  pmapglb2xN  38281  paddasslem14  38342  cdleme27a  38876  sdomne0  41773  sdomne0d  41774  iccpartigtl  45701
  Copyright terms: Public domain W3C validator