Theorem pm2.61dne 3020

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

Syntax hints:   → wi 4   = wceq 1547   ≠ wne 2934

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 208  df-ne 2935

This theorem is referenced by:  pm2.61dane  3021  wefrc  5612  wereu2  5615  frpomin  6291  oe0lem  8438  fisupg  9188  marypha1lem  9336  fiinfg  9404  wdomtr  9480  unxpwdom2  9493  frmin  9664  fpwwe2lem12  10556  grur1a  10733  grutsk  10736  fimaxre2  12092  xlesubadd  13206  cshwidxmod  14756  sqreu  15314  pcxnn0cl  16822  pcxcl  16823  pcmpt  16854  symggen  19436  isabvd  20784  lspprat  21146  mdetralt  22591  ordtrest2lem  23186  ordthauslem  23366  comppfsc  23515  fbssint  23821  fclscf  24008  tgptsmscld  24134  ovoliunnul  25492  itg11  25676  i1fadd  25680  fta1g  26153  plydiveu  26282  fta1  26292  mulcxp  26667  cxpsqrt  26685  ostth3  27619  madebdaylemlrcut  27909  brbtwn2  28992  colinearalg  28997  clwwisshclwws  30103  ordtrest2NEWlem  34106  fissorduni  35271  subfacp1lem5  35412  btwnexch2  36251  fnemeet2  36595  fnejoin2  36597  limsucncmpi  36673  areacirc  38080  sstotbnd2  38141  ssbnd  38155  prdsbnd2  38162  rrncmslem  38199  atnlt  39805  atlelt  39930  llnnlt  40015  lplnnlt  40057  lvolnltN  40110  pmapglb2N  40263  pmapglb2xN  40264  paddasslem14  40325  cdleme27a  40859  sdomne0  43857  sdomne0d  43858  modelaxreplem1  45422  iccpartigtl  47898