Theorem pm2.61dne 3030

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  pm2.61dane  3031  wefrc  5574  wereu2  5577  frpomin  6228  oe0lem  8305  fisupg  8992  marypha1lem  9122  fiinfg  9188  wdomtr  9264  unxpwdom2  9277  frmin  9438  fpwwe2lem12  10329  grur1a  10506  grutsk  10509  fimaxre2  11850  xlesubadd  12926  cshwidxmod  14444  sqreu  15000  pcxnn0cl  16489  pcxcl  16490  pcmpt  16521  symggen  18993  isabvd  19995  lspprat  20330  mdetralt  21665  ordtrest2lem  22262  ordthauslem  22442  comppfsc  22591  fbssint  22897  fclscf  23084  tgptsmscld  23210  ovoliunnul  24576  itg11  24760  i1fadd  24764  fta1g  25237  plydiveu  25363  fta1  25373  mulcxp  25745  cxpsqrt  25763  ostth3  26691  brbtwn2  27176  colinearalg  27181  clwwisshclwws  28280  ordtrest2NEWlem  31774  subfacp1lem5  33046  madebdaylemlrcut  34006  btwnexch2  34252  fnemeet2  34483  fnejoin2  34485  limsucncmpi  34561  areacirc  35797  sstotbnd2  35859  ssbnd  35873  prdsbnd2  35880  rrncmslem  35917  atnlt  37254  atlelt  37379  llnnlt  37464  lplnnlt  37506  lvolnltN  37559  pmapglb2N  37712  pmapglb2xN  37713  paddasslem14  37774  cdleme27a  38308  iccpartigtl  44763