Theorem pm2.61dne 3034

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  pm2.61dane  3035  wefrc  5694  wereu2  5697  frpomin  6372  oe0lem  8569  fisupg  9352  marypha1lem  9502  fiinfg  9568  wdomtr  9644  unxpwdom2  9657  frmin  9818  fpwwe2lem12  10711  grur1a  10888  grutsk  10891  fimaxre2  12240  xlesubadd  13325  cshwidxmod  14851  sqreu  15409  pcxnn0cl  16907  pcxcl  16908  pcmpt  16939  symggen  19512  isabvd  20835  lspprat  21178  mdetralt  22635  ordtrest2lem  23232  ordthauslem  23412  comppfsc  23561  fbssint  23867  fclscf  24054  tgptsmscld  24180  ovoliunnul  25561  itg11  25745  i1fadd  25749  fta1g  26229  plydiveu  26358  fta1  26368  mulcxp  26745  cxpsqrt  26763  ostth3  27700  madebdaylemlrcut  27955  brbtwn2  28938  colinearalg  28943  clwwisshclwws  30047  ordtrest2NEWlem  33868  subfacp1lem5  35152  btwnexch2  35987  fnemeet2  36333  fnejoin2  36335  limsucncmpi  36411  areacirc  37673  sstotbnd2  37734  ssbnd  37748  prdsbnd2  37755  rrncmslem  37792  atnlt  39269  atlelt  39395  llnnlt  39480  lplnnlt  39522  lvolnltN  39575  pmapglb2N  39728  pmapglb2xN  39729  paddasslem14  39790  cdleme27a  40324  sdomne0  43375  sdomne0d  43376  iccpartigtl  47297