Theorem pm2.61dne 3011

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

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

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 2926

This theorem is referenced by:  pm2.61dane  3012  wefrc  5613  wereu2  5616  frpomin  6288  oe0lem  8431  fisupg  9177  marypha1lem  9323  fiinfg  9391  wdomtr  9467  unxpwdom2  9480  frmin  9645  fpwwe2lem12  10536  grur1a  10713  grutsk  10716  fimaxre2  12070  xlesubadd  13165  cshwidxmod  14709  sqreu  15268  pcxnn0cl  16772  pcxcl  16773  pcmpt  16804  symggen  19349  isabvd  20697  lspprat  21060  mdetralt  22493  ordtrest2lem  23088  ordthauslem  23268  comppfsc  23417  fbssint  23723  fclscf  23910  tgptsmscld  24036  ovoliunnul  25406  itg11  25590  i1fadd  25594  fta1g  26073  plydiveu  26204  fta1  26214  mulcxp  26592  cxpsqrt  26610  ostth3  27547  madebdaylemlrcut  27813  brbtwn2  28850  colinearalg  28855  clwwisshclwws  29959  ordtrest2NEWlem  33889  subfacp1lem5  35157  btwnexch2  35997  fnemeet2  36341  fnejoin2  36343  limsucncmpi  36419  areacirc  37693  sstotbnd2  37754  ssbnd  37768  prdsbnd2  37775  rrncmslem  37812  atnlt  39292  atlelt  39417  llnnlt  39502  lplnnlt  39544  lvolnltN  39597  pmapglb2N  39750  pmapglb2xN  39751  paddasslem14  39812  cdleme27a  40346  sdomne0  43386  sdomne0d  43387  modelaxreplem1  44952  iccpartigtl  47407