Theorem pm2.61dne 3032

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2944

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 2945

This theorem is referenced by:  pm2.61dane  3033  wefrc  5584  wereu2  5587  frpomin  6247  oe0lem  8352  fisupg  9071  marypha1lem  9201  fiinfg  9267  wdomtr  9343  unxpwdom2  9356  frmin  9516  fpwwe2lem12  10407  grur1a  10584  grutsk  10587  fimaxre2  11929  xlesubadd  13006  cshwidxmod  14525  sqreu  15081  pcxnn0cl  16570  pcxcl  16571  pcmpt  16602  symggen  19087  isabvd  20089  lspprat  20424  mdetralt  21766  ordtrest2lem  22363  ordthauslem  22543  comppfsc  22692  fbssint  22998  fclscf  23185  tgptsmscld  23311  ovoliunnul  24680  itg11  24864  i1fadd  24868  fta1g  25341  plydiveu  25467  fta1  25477  mulcxp  25849  cxpsqrt  25867  ostth3  26795  brbtwn2  27282  colinearalg  27287  clwwisshclwws  28388  ordtrest2NEWlem  31881  subfacp1lem5  33155  madebdaylemlrcut  34088  btwnexch2  34334  fnemeet2  34565  fnejoin2  34567  limsucncmpi  34643  areacirc  35879  sstotbnd2  35941  ssbnd  35955  prdsbnd2  35962  rrncmslem  35999  atnlt  37334  atlelt  37459  llnnlt  37544  lplnnlt  37586  lvolnltN  37639  pmapglb2N  37792  pmapglb2xN  37793  paddasslem14  37854  cdleme27a  38388  iccpartigtl  44886