Theorem pm2.61dne 3014

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  pm2.61dane  3015  wefrc  5613  wereu2  5616  frpomin  6293  oe0lem  8434  fisupg  9178  marypha1lem  9323  fiinfg  9391  wdomtr  9467  unxpwdom2  9480  frmin  9648  fpwwe2lem12  10539  grur1a  10716  grutsk  10719  fimaxre2  12073  xlesubadd  13168  cshwidxmod  14716  sqreu  15274  pcxnn0cl  16778  pcxcl  16779  pcmpt  16810  symggen  19388  isabvd  20733  lspprat  21096  mdetralt  22529  ordtrest2lem  23124  ordthauslem  23304  comppfsc  23453  fbssint  23759  fclscf  23946  tgptsmscld  24072  ovoliunnul  25441  itg11  25625  i1fadd  25629  fta1g  26108  plydiveu  26239  fta1  26249  mulcxp  26627  cxpsqrt  26645  ostth3  27582  madebdaylemlrcut  27850  brbtwn2  28890  colinearalg  28895  clwwisshclwws  30002  ordtrest2NEWlem  33942  fissorduni  35108  subfacp1lem5  35235  btwnexch2  36074  fnemeet2  36418  fnejoin2  36420  limsucncmpi  36496  areacirc  37759  sstotbnd2  37820  ssbnd  37834  prdsbnd2  37841  rrncmslem  37878  atnlt  39418  atlelt  39543  llnnlt  39628  lplnnlt  39670  lvolnltN  39723  pmapglb2N  39876  pmapglb2xN  39877  paddasslem14  39938  cdleme27a  40472  sdomne0  43511  sdomne0d  43512  modelaxreplem1  45076  iccpartigtl  47528