Theorem pm2.61dne 3012

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 3009	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2926

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 2927

This theorem is referenced by:  pm2.61dane  3013  wefrc  5635  wereu2  5638  frpomin  6316  oe0lem  8480  fisupg  9242  marypha1lem  9391  fiinfg  9459  wdomtr  9535  unxpwdom2  9548  frmin  9709  fpwwe2lem12  10602  grur1a  10779  grutsk  10782  fimaxre2  12135  xlesubadd  13230  cshwidxmod  14775  sqreu  15334  pcxnn0cl  16838  pcxcl  16839  pcmpt  16870  symggen  19407  isabvd  20728  lspprat  21070  mdetralt  22502  ordtrest2lem  23097  ordthauslem  23277  comppfsc  23426  fbssint  23732  fclscf  23919  tgptsmscld  24045  ovoliunnul  25415  itg11  25599  i1fadd  25603  fta1g  26082  plydiveu  26213  fta1  26223  mulcxp  26601  cxpsqrt  26619  ostth3  27556  madebdaylemlrcut  27817  brbtwn2  28839  colinearalg  28844  clwwisshclwws  29951  ordtrest2NEWlem  33919  subfacp1lem5  35178  btwnexch2  36018  fnemeet2  36362  fnejoin2  36364  limsucncmpi  36440  areacirc  37714  sstotbnd2  37775  ssbnd  37789  prdsbnd2  37796  rrncmslem  37833  atnlt  39313  atlelt  39439  llnnlt  39524  lplnnlt  39566  lvolnltN  39619  pmapglb2N  39772  pmapglb2xN  39773  paddasslem14  39834  cdleme27a  40368  sdomne0  43409  sdomne0d  43410  modelaxreplem1  44975  iccpartigtl  47428