Theorem pm2.61ne 3018

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

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

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 2934

This theorem is referenced by:  pwdom  9069  cantnfle  9592  cantnflem1  9610  cantnf  9614  djulepw  10115  infmap2  10139  zornn0g  10427  ttukeylem6  10436  msqge0  11670  xrsupsslem  13234  xrinfmsslem  13235  fzoss1  13614  swrdcl  14581  pfxcl  14613  abs1m  15271  fsumcvg3  15664  bezoutlem4  16481  dvdssq  16506  lcmid  16548  pcdvdsb  16809  pcgcd1  16817  pc2dvds  16819  pcaddlem  16828  qexpz  16841  4sqlem19  16903  prmlem1a  17046  gsumwsubmcl  18774  gsumccat  18778  gsumwmhm  18782  cntzsdrg  20747  zringlpir  21434  psdmul  22121  mretopd  23048  ufildom1  23882  alexsublem  24000  nmolb2d  24674  nmoi  24684  nmoix  24685  ipcau2  25202  mdegcl  26042  ply1divex  26110  ig1pcl  26152  dgrmulc  26245  mulcxplem  26661  vmacl  27096  efvmacl  27098  vmalelog  27184  padicabv  27609  nmlnoubi  30884  nmblolbii  30887  blocnilem  30892  blocni  30893  ubthlem1  30958  nmbdoplbi  32112  cnlnadjlem7  32161  branmfn  32193  pjbdlni  32237  shatomistici  32449  segcon2  36321  lssats  39388  ps-1  39853  3atlem5  39863  lplnnle2at  39917  2llnm3N  39945  lvolnle3at  39958  4atex2  40453  cdlemd5  40578  cdleme21k  40714  cdlemg33b  41083  mapdrvallem2  42021  mapdhcl  42103  hdmapval3N  42214  hdmap10  42216  hdmaprnlem17N  42239  hdmap14lem2a  42243  hdmaplkr  42289  hgmapvv  42302  explt1d  42693  fiabv  42906