Theorem pm2.61ne 3041

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

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

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 2957

This theorem is used by:  pwdom  9148  cantnfle  9672  cantnflem1  9690  cantnf  9694  djulepw  10271  infmap2  10295  zornn0g  10583  ttukeylem6  10592  msqge0  11837  xrsupsslem  13437  xrinfmsslem  13438  fzoss1  13821  swrdcl  14793  pfxcl  14827  abs1m  15503  fsumcvg3  15895  bezoutlem4  16715  dvdssq  16742  lcmid  16784  pcdvdsb  17047  pcgcd1  17055  pc2dvds  17057  pcaddlem  17066  qexpz  17079  4sqlem19  17141  prmlem1a  17284  gsumwsubmcl  19033  gsumccat  19037  gsumwmhm  19041  cntzsdrg  21059  zringlpir  21773  psdmul  22487  mretopd  23410  ufildom1  24245  alexsublem  24363  nmolb2d  25037  nmoi  25047  nmoix  25048  ipcau2  25555  mdegcl  26387  ply1divex  26455  ig1pcl  26497  dgrmulc  26590  mulcxplem  27012  vmacl  27445  efvmacl  27447  vmalelog  27532  padicabv  27957  nmlnoubi  31398  nmblolbii  31401  blocnilem  31406  blocni  31407  ubthlem1  31472  nmbdoplbi  32626  cnlnadjlem7  32675  branmfn  32707  pjbdlni  32751  shatomistici  32963  segcon2  36870  mh-inf3f1  37329  lssats  40069  ps-1  40534  3atlem5  40544  lplnnle2at  40598  2llnm3N  40626  lvolnle3at  40639  4atex2  41134  cdlemd5  41259  cdleme21k  41395  cdlemg33b  41764  mapdrvallem2  42702  mapdhcl  42784  hdmapval3N  42895  hdmap10  42897  hdmaprnlem17N  42920  hdmap14lem2a  42924  hdmaplkr  42970  hgmapvv  42983  explt1d  43380  fiabv  43600