Theorem pm2.61dne 3027

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

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

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 2940

This theorem is referenced by:  pm2.61dane  3028  wefrc  5632  wereu2  5635  frpomin  6299  oe0lem  8464  fisupg  9242  marypha1lem  9378  fiinfg  9444  wdomtr  9520  unxpwdom2  9533  frmin  9694  fpwwe2lem12  10587  grur1a  10764  grutsk  10767  fimaxre2  12109  xlesubadd  13192  cshwidxmod  14703  sqreu  15257  pcxnn0cl  16743  pcxcl  16744  pcmpt  16775  symggen  19266  isabvd  20335  lspprat  20673  mdetralt  21994  ordtrest2lem  22591  ordthauslem  22771  comppfsc  22920  fbssint  23226  fclscf  23413  tgptsmscld  23539  ovoliunnul  24908  itg11  25092  i1fadd  25096  fta1g  25569  plydiveu  25695  fta1  25705  mulcxp  26077  cxpsqrt  26095  ostth3  27023  madebdaylemlrcut  27271  brbtwn2  27917  colinearalg  27922  clwwisshclwws  29022  ordtrest2NEWlem  32592  subfacp1lem5  33865  btwnexch2  34684  fnemeet2  34915  fnejoin2  34917  limsucncmpi  34993  areacirc  36244  sstotbnd2  36306  ssbnd  36320  prdsbnd2  36327  rrncmslem  36364  atnlt  37848  atlelt  37974  llnnlt  38059  lplnnlt  38101  lvolnltN  38154  pmapglb2N  38307  pmapglb2xN  38308  paddasslem14  38369  cdleme27a  38903  sdomne0  41807  sdomne0d  41808  iccpartigtl  45735