Theorem pm2.61dne 3044

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

Syntax hints:   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  pm2.61dane  3045  wefrc  5655  wereu2  5658  frpomin  6341  oe0lem  8494  fisupg  9244  marypha1lem  9389  fiinfg  9457  wdomtr  9533  unxpwdom2  9546  frmin  9717  fpwwe2lem12  10622  grur1a  10799  grutsk  10802  fimaxre2  12155  xlesubadd  13284  cshwidxmod  14836  sqreu  15408  pcxnn0cl  16915  pcxcl  16916  pcmpt  16947  symggen  19535  isabvd  20915  lspprat  21277  mdetralt  22765  ordtrest2lem  23360  ordthauslem  23540  comppfsc  23689  fbssint  23995  fclscf  24182  tgptsmscld  24308  ovoliunnul  25666  itg11  25850  i1fadd  25854  fta1g  26327  plydiveu  26459  fta1  26469  mulcxp  26850  cxpsqrt  26868  ostth3  27802  madebdaylemlrcut  28092  brbtwn2  29255  colinearalg  29260  clwwisshclwws  30366  ordtrest2NEWlem  34312  fissorduni  35480  subfacp1lem5  35676  btwnexch2  36515  fnemeet2  36878  fnejoin2  36880  limsucncmpi  36956  areacirc  38364  sstotbnd2  38425  ssbnd  38439  prdsbnd2  38446  rrncmslem  38483  atnlt  40087  atlelt  40212  llnnlt  40297  lplnnlt  40339  lvolnltN  40392  pmapglb2N  40545  pmapglb2xN  40546  paddasslem14  40607  cdleme27a  41141  sdomne0  44139  sdomne0d  44140  modelaxreplem1  45687  iccpartigtl  48172