Theorem pm2.61dne 3018

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

Syntax hints:   → wi 4   = wceq 1534   ≠ wne 2930

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 2931

This theorem is referenced by:  pm2.61dane  3019  wefrc  5668  wereu2  5671  frpomin  6345  oe0lem  8535  fisupg  9318  marypha1lem  9469  fiinfg  9535  wdomtr  9611  unxpwdom2  9624  frmin  9785  fpwwe2lem12  10676  grur1a  10853  grutsk  10856  fimaxre2  12205  xlesubadd  13290  cshwidxmod  14806  sqreu  15360  pcxnn0cl  16857  pcxcl  16858  pcmpt  16889  symggen  19464  isabvd  20787  lspprat  21130  mdetralt  22598  ordtrest2lem  23195  ordthauslem  23375  comppfsc  23524  fbssint  23830  fclscf  24017  tgptsmscld  24143  ovoliunnul  25524  itg11  25708  i1fadd  25712  fta1g  26194  plydiveu  26323  fta1  26333  mulcxp  26709  cxpsqrt  26727  ostth3  27664  madebdaylemlrcut  27919  brbtwn2  28836  colinearalg  28841  clwwisshclwws  29945  ordtrest2NEWlem  33750  subfacp1lem5  35025  btwnexch2  35860  fnemeet2  36092  fnejoin2  36094  limsucncmpi  36170  areacirc  37427  sstotbnd2  37488  ssbnd  37502  prdsbnd2  37509  rrncmslem  37546  atnlt  39024  atlelt  39150  llnnlt  39235  lplnnlt  39277  lvolnltN  39330  pmapglb2N  39483  pmapglb2xN  39484  paddasslem14  39545  cdleme27a  40079  sdomne0  43117  sdomne0d  43118  iccpartigtl  47031