Theorem pm2.61ne 3016

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ≠ wne 2929

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-an 395  df-ne 2930

This theorem is referenced by:  pwdom  9157  cantnfle  9701  cantnflem1  9719  cantnf  9723  djulepw  10222  infmap2  10248  zornn0g  10535  ttukeylem6  10544  msqge0  11772  xrsupsslem  13326  xrinfmsslem  13327  fzoss1  13699  swrdcl  14639  pfxcl  14671  abs1m  15326  fsumcvg3  15719  bezoutlem4  16529  dvdssq  16554  lcmid  16596  pcdvdsb  16857  pcgcd1  16865  pc2dvds  16867  pcaddlem  16876  qexpz  16889  4sqlem19  16951  prmlem1a  17095  gsumwsubmcl  18813  gsumccat  18817  gsumwmhm  18821  cntzsdrg  20719  zringlpir  21427  psdmul  22130  mretopd  23057  ufildom1  23891  alexsublem  24009  nmolb2d  24696  nmoi  24706  nmoix  24707  ipcau2  25223  mdegcl  26066  ply1divex  26134  ig1pcl  26175  dgrmulc  26268  mulcxplem  26680  vmacl  27115  efvmacl  27117  vmalelog  27203  padicabv  27628  nmlnoubi  30698  nmblolbii  30701  blocnilem  30706  blocni  30707  ubthlem1  30772  nmbdoplbi  31926  cnlnadjlem7  31975  branmfn  32007  pjbdlni  32051  shatomistici  32263  segcon2  35852  lssats  38634  ps-1  39100  3atlem5  39110  lplnnle2at  39164  2llnm3N  39192  lvolnle3at  39205  4atex2  39700  cdlemd5  39825  cdleme21k  39961  cdlemg33b  40330  mapdrvallem2  41268  mapdhcl  41350  hdmapval3N  41461  hdmap10  41463  hdmaprnlem17N  41486  hdmap14lem2a  41490  hdmaplkr  41536  hgmapvv  41549