Theorem pm2.61dne 3105

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3018

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 209  df-ne 3019

This theorem is referenced by:  pm2.61dane  3106  wefrc  5551  wereu2  5554  oe0lem  8140  fisupg  8768  marypha1lem  8899  fiinfg  8965  wdomtr  9041  unxpwdom2  9054  fpwwe2lem13  10066  grur1a  10243  grutsk  10246  fimaxre2  11588  xlesubadd  12659  cshwidxmod  14167  sqreu  14722  pcxcl  16199  pcmpt  16230  symggen  18600  isabvd  19593  lspprat  19927  mdetralt  21219  ordtrest2lem  21813  ordthauslem  21993  comppfsc  22142  fbssint  22448  fclscf  22635  tgptsmscld  22761  ovoliunnul  24110  itg11  24294  i1fadd  24298  fta1g  24763  plydiveu  24889  fta1  24899  mulcxp  25270  cxpsqrt  25288  ostth3  26216  brbtwn2  26693  colinearalg  26698  clwwisshclwws  27795  ordtrest2NEWlem  31167  subfacp1lem5  32433  frpomin  33080  frmin  33086  btwnexch2  33486  fnemeet2  33717  fnejoin2  33719  limsucncmpi  33795  areacirc  34989  sstotbnd2  35054  ssbnd  35068  prdsbnd2  35075  rrncmslem  35112  atnlt  36451  atlelt  36576  llnnlt  36661  lplnnlt  36703  lvolnltN  36756  pmapglb2N  36909  pmapglb2xN  36910  paddasslem14  36971  cdleme27a  37505  iccpartigtl  43590