Theorem pm2.61dne 3018

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

Step	Hyp	Ref	Expression
1		pm2.61dne.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
2	1	com12 32	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓))
3		pm2.61dne.2	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
4	3	com12 32	. 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓))
5	2, 4	pm2.61ine 3015	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  pm2.61dane  3019  wefrc  5625  wereu2  5628  frpomin  6304  oe0lem  8448  fisupg  9198  marypha1lem  9346  fiinfg  9414  wdomtr  9490  unxpwdom2  9503  frmin  9673  fpwwe2lem12  10565  grur1a  10742  grutsk  10745  fimaxre2  12101  xlesubadd  13215  cshwidxmod  14765  sqreu  15323  pcxnn0cl  16831  pcxcl  16832  pcmpt  16863  symggen  19445  isabvd  20789  lspprat  21151  mdetralt  22573  ordtrest2lem  23168  ordthauslem  23348  comppfsc  23497  fbssint  23803  fclscf  23990  tgptsmscld  24116  ovoliunnul  25474  itg11  25658  i1fadd  25662  fta1g  26135  plydiveu  26264  fta1  26274  mulcxp  26649  cxpsqrt  26667  ostth3  27601  madebdaylemlrcut  27891  brbtwn2  28974  colinearalg  28979  clwwisshclwws  30085  ordtrest2NEWlem  34066  fissorduni  35233  subfacp1lem5  35366  btwnexch2  36205  fnemeet2  36549  fnejoin2  36551  limsucncmpi  36627  areacirc  38034  sstotbnd2  38095  ssbnd  38109  prdsbnd2  38116  rrncmslem  38153  atnlt  39759  atlelt  39884  llnnlt  39969  lplnnlt  40011  lvolnltN  40064  pmapglb2N  40217  pmapglb2xN  40218  paddasslem14  40279  cdleme27a  40813  sdomne0  43840  sdomne0d  43841  modelaxreplem1  45405  iccpartigtl  47883