Theorem pm2.61dne 3042

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 33	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓))
3		pm2.61dne.2	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
4	3	com12 33	. 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓))
5	2, 4	pm2.61ine 3039	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  pm2.61dane  3043  wefrc  5645  wereu2  5648  frpomin  6342  oe0lem  8514  fisupg  9272  fissorduni  9275  marypha1lem  9418  fiinfg  9486  wdomtr  9562  unxpwdom2  9575  frmin  9746  fpwwe2lem12  10720  grur1a  10897  grutsk  10900  fimaxre2  12255  xlesubadd  13386  cshwidxmod  14947  sqreu  15521  pcxnn0cl  17031  pcxcl  17032  pcmpt  17063  symggen  19677  isabvd  21062  lspprat  21424  mdetralt  22916  ordtrest2lem  23514  ordthauslem  23694  comppfsc  23844  fbssint  24150  fclscf  24337  tgptsmscld  24463  ovoliunnul  25821  itg11  26005  i1fadd  26009  fta1g  26481  plydiveu  26612  fta1  26622  mulcxp  27006  cxpsqrt  27024  ostth3  27958  madebdaylemlrcut  28278  brbtwn2  29476  colinearalg  29481  clwwisshclwws  30599  ordtrest2NEWlem  34547  subfacp1lem5  35928  btwnexch2  36768  fnemeet2  37135  fnejoin2  37137  limsucncmpi  37213  areacirc  38611  sstotbnd2  38688  ssbnd  38702  prdsbnd2  38709  rrncmslem  38746  atnlt  40350  atlelt  40475  llnnlt  40560  lplnnlt  40602  lvolnltN  40655  pmapglb2N  40808  pmapglb2xN  40809  paddasslem14  40870  cdleme27a  41404  sdomne0  44398  sdomne0d  44399  modelaxreplem1  45946  iccpartigtl  48474