Theorem pm2.61ne 3025

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

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

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 2939

This theorem is referenced by:  pwdom  9131  cantnfle  9668  cantnflem1  9686  cantnf  9690  djulepw  10189  infmap2  10215  zornn0g  10502  ttukeylem6  10511  msqge0  11739  xrsupsslem  13290  xrinfmsslem  13291  fzoss1  13663  swrdcl  14599  pfxcl  14631  abs1m  15286  fsumcvg3  15679  bezoutlem4  16488  dvdssq  16508  lcmid  16550  pcdvdsb  16806  pcgcd1  16814  pc2dvds  16816  pcaddlem  16825  qexpz  16838  4sqlem19  16900  prmlem1a  17044  gsumwsubmcl  18754  gsumccat  18758  gsumwmhm  18762  cntzsdrg  20561  zringlpir  21238  mretopd  22816  ufildom1  23650  alexsublem  23768  nmolb2d  24455  nmoi  24465  nmoix  24466  ipcau2  24982  mdegcl  25822  ply1divex  25889  ig1pcl  25928  dgrmulc  26021  mulcxplem  26428  vmacl  26858  efvmacl  26860  vmalelog  26944  padicabv  27369  nmlnoubi  30316  nmblolbii  30319  blocnilem  30324  blocni  30325  ubthlem1  30390  nmbdoplbi  31544  cnlnadjlem7  31593  branmfn  31625  pjbdlni  31669  shatomistici  31881  segcon2  35381  lssats  38185  ps-1  38651  3atlem5  38661  lplnnle2at  38715  2llnm3N  38743  lvolnle3at  38756  4atex2  39251  cdlemd5  39376  cdleme21k  39512  cdlemg33b  39881  mapdrvallem2  40819  mapdhcl  40901  hdmapval3N  41012  hdmap10  41014  hdmaprnlem17N  41037  hdmap14lem2a  41041  hdmaplkr  41087  hgmapvv  41100