Theorem pm2.61ne 3043

Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)

Hypotheses

Ref	Expression
pm2.61ne.1	⊢ (𝐴 = 𝐵 → (𝜓 ↔ 𝜒))
pm2.61ne.2	⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
pm2.61ne.3	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
pm2.61ne	⊢ (𝜑 → 𝜓)

Proof of Theorem pm2.61ne

Step	Hyp	Ref	Expression
1		pm2.61ne.3	. . 3 ⊢ (𝜑 → 𝜒)
2		pm2.61ne.1	. . 3 ⊢ (𝐴 = 𝐵 → (𝜓 ↔ 𝜒))
3	1, 2	imbitrrid 249	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓))
4		pm2.61ne.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
5	4	expcom 419	. 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓))
6	3, 5	pm2.61ine 3041	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ≠ wne 2958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-ne 2959

This theorem is used by:  pwdom  9159  cantnfle  9682  cantnflem1  9700  cantnf  9704  djulepw  10281  infmap2  10305  zornn0g  10593  ttukeylem6  10602  msqge0  11847  xrsupsslem  13447  xrinfmsslem  13448  fzoss1  13831  swrdcl  14804  pfxcl  14838  abs1m  15515  fsumcvg3  15907  bezoutlem4  16727  dvdssq  16754  lcmid  16796  pcdvdsb  17059  pcgcd1  17067  pc2dvds  17069  pcaddlem  17078  qexpz  17091  4sqlem19  17153  prmlem1a  17296  gsumwsubmcl  19045  gsumccat  19049  gsumwmhm  19053  cntzsdrg  21071  zringlpir  21785  psdmul  22499  mretopd  23422  ufildom1  24257  alexsublem  24375  nmolb2d  25049  nmoi  25059  nmoix  25060  ipcau2  25567  mdegcl  26399  ply1divex  26467  ig1pcl  26509  dgrmulc  26602  mulcxplem  27024  vmacl  27457  efvmacl  27459  vmalelog  27544  padicabv  27969  nmlnoubi  31410  nmblolbii  31413  blocnilem  31418  blocni  31419  ubthlem1  31484  nmbdoplbi  32638  cnlnadjlem7  32687  branmfn  32719  pjbdlni  32763  shatomistici  32975  segcon2  36997  mh-inf3f1  37456  lssats  40209  ps-1  40674  3atlem5  40684  lplnnle2at  40738  2llnm3N  40766  lvolnle3at  40779  4atex2  41274  cdlemd5  41399  cdleme21k  41535  cdlemg33b  41904  mapdrvallem2  42842  mapdhcl  42924  hdmapval3N  43035  hdmap10  43037  hdmaprnlem17N  43060  hdmap14lem2a  43064  hdmaplkr  43110  hgmapvv  43123  explt1d  43520  fiabv  43740