Theorem pm2.61dne 3071

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.2	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
2		nne 2989	. . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)
3		pm2.61dne.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
4	2, 3	syl5bi 233	. 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓))
5	1, 4	pm2.61d 171	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1637   ≠ wne 2985

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 198  df-ne 2986

This theorem is referenced by:  pm2.61dane  3072  wefrc  5312  wereu2  5315  oe0lem  7833  fisupg  8450  marypha1lem  8581  fiinfg  8647  wdomtr  8722  unxpwdom2  8735  fpwwe2lem13  9752  grur1a  9929  grutsk  9932  fimaxre2  11257  xlesubadd  12314  cshwidxmod  13776  sqreu  14326  pcxcl  15785  pcmpt  15816  symggen  18094  isabvd  19027  lspprat  19365  mdetralt  20629  ordtrest2lem  21225  ordthauslem  21405  comppfsc  21553  fbssint  21859  fclscf  22046  tgptsmscld  22171  ovoliunnul  23494  itg11  23678  i1fadd  23682  fta1g  24147  plydiveu  24273  fta1  24283  mulcxp  24651  cxpsqrt  24669  ostth3  25547  brbtwn2  26005  colinearalg  26010  clwwisshclwws  27164  ordtrest2NEWlem  30299  subfacp1lem5  31494  frpomin  32064  frmin  32068  btwnexch2  32456  fnemeet2  32688  fnejoin2  32690  limsucncmpi  32766  areacirc  33819  sstotbnd2  33886  ssbnd  33900  prdsbnd2  33907  rrncmslem  33944  atnlt  35095  atlelt  35220  llnnlt  35305  lplnnlt  35347  lvolnltN  35400  pmapglb2N  35553  pmapglb2xN  35554  paddasslem14  35615  cdleme27a  36149  iccpartigtl  41935