Theorem pm2.61dne 3028

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2940

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 2941

This theorem is referenced by:  pm2.61dane  3029  wefrc  5614  wereu2  5617  frpomin  6279  oe0lem  8414  fisupg  9156  marypha1lem  9290  fiinfg  9356  wdomtr  9432  unxpwdom2  9445  frmin  9606  fpwwe2lem12  10499  grur1a  10676  grutsk  10679  fimaxre2  12021  xlesubadd  13098  cshwidxmod  14614  sqreu  15171  pcxnn0cl  16658  pcxcl  16659  pcmpt  16690  symggen  19174  isabvd  20186  lspprat  20521  mdetralt  21863  ordtrest2lem  22460  ordthauslem  22640  comppfsc  22789  fbssint  23095  fclscf  23282  tgptsmscld  23408  ovoliunnul  24777  itg11  24961  i1fadd  24965  fta1g  25438  plydiveu  25564  fta1  25574  mulcxp  25946  cxpsqrt  25964  ostth3  26892  brbtwn2  27562  colinearalg  27567  clwwisshclwws  28667  ordtrest2NEWlem  32170  subfacp1lem5  33445  madebdaylemlrcut  34175  btwnexch2  34421  fnemeet2  34652  fnejoin2  34654  limsucncmpi  34730  areacirc  35975  sstotbnd2  36037  ssbnd  36051  prdsbnd2  36058  rrncmslem  36095  atnlt  37580  atlelt  37706  llnnlt  37791  lplnnlt  37833  lvolnltN  37886  pmapglb2N  38039  pmapglb2xN  38040  paddasslem14  38101  cdleme27a  38635  sdomne0  41342  sdomne0d  41343  iccpartigtl  45226