Theorem pm2.61ne 3013

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 246	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓))
4		pm2.61ne.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
5	4	expcom 413	. 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓))
6	3, 5	pm2.61ine 3011	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ≠ wne 2928

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-an 396  df-ne 2929

This theorem is referenced by:  pwdom  9042  cantnfle  9561  cantnflem1  9579  cantnf  9583  djulepw  10084  infmap2  10108  zornn0g  10396  ttukeylem6  10405  msqge0  11638  xrsupsslem  13206  xrinfmsslem  13207  fzoss1  13586  swrdcl  14553  pfxcl  14585  abs1m  15243  fsumcvg3  15636  bezoutlem4  16453  dvdssq  16478  lcmid  16520  pcdvdsb  16781  pcgcd1  16789  pc2dvds  16791  pcaddlem  16800  qexpz  16813  4sqlem19  16875  prmlem1a  17018  gsumwsubmcl  18745  gsumccat  18749  gsumwmhm  18753  cntzsdrg  20717  zringlpir  21404  psdmul  22081  mretopd  23007  ufildom1  23841  alexsublem  23959  nmolb2d  24633  nmoi  24643  nmoix  24644  ipcau2  25161  mdegcl  26001  ply1divex  26069  ig1pcl  26111  dgrmulc  26204  mulcxplem  26620  vmacl  27055  efvmacl  27057  vmalelog  27143  padicabv  27568  nmlnoubi  30776  nmblolbii  30779  blocnilem  30784  blocni  30785  ubthlem1  30850  nmbdoplbi  32004  cnlnadjlem7  32053  branmfn  32085  pjbdlni  32129  shatomistici  32341  segcon2  36149  lssats  39121  ps-1  39586  3atlem5  39596  lplnnle2at  39650  2llnm3N  39678  lvolnle3at  39691  4atex2  40186  cdlemd5  40311  cdleme21k  40447  cdlemg33b  40816  mapdrvallem2  41754  mapdhcl  41836  hdmapval3N  41947  hdmap10  41949  hdmaprnlem17N  41972  hdmap14lem2a  41976  hdmaplkr  42022  hgmapvv  42035  explt1d  42426  fiabv  42639