Theorem pm2.61ne 3029

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

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

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 396  df-ne 2943

This theorem is referenced by:  pwdom  8865  cantnfle  9359  cantnflem1  9377  cantnf  9381  djulepw  9879  infmap2  9905  zornn0g  10192  ttukeylem6  10201  msqge0  11426  xrsupsslem  12970  xrinfmsslem  12971  fzoss1  13342  swrdcl  14286  pfxcl  14318  abs1m  14975  fsumcvg3  15369  bezoutlem4  16178  gcdmultiplezOLD  16189  dvdssq  16200  lcmid  16242  pcdvdsb  16498  pcgcd1  16506  pc2dvds  16508  pcaddlem  16517  qexpz  16530  4sqlem19  16592  prmlem1a  16736  gsumwsubmcl  18390  gsumccatOLD  18394  gsumccat  18395  gsumwmhm  18399  cntzsdrg  19985  zringlpir  20601  mretopd  22151  ufildom1  22985  alexsublem  23103  nmolb2d  23788  nmoi  23798  nmoix  23799  ipcau2  24303  mdegcl  25139  ply1divex  25206  ig1pcl  25245  dgrmulc  25337  mulcxplem  25744  vmacl  26172  efvmacl  26174  vmalelog  26258  padicabv  26683  nmlnoubi  29059  nmblolbii  29062  blocnilem  29067  blocni  29068  ubthlem1  29133  nmbdoplbi  30287  cnlnadjlem7  30336  branmfn  30368  pjbdlni  30412  shatomistici  30624  segcon2  34334  lssats  36953  ps-1  37418  3atlem5  37428  lplnnle2at  37482  2llnm3N  37510  lvolnle3at  37523  4atex2  38018  cdlemd5  38143  cdleme21k  38279  cdlemg33b  38648  mapdrvallem2  39586  mapdhcl  39668  hdmapval3N  39779  hdmap10  39781  hdmaprnlem17N  39804  hdmap14lem2a  39808  hdmaplkr  39854  hgmapvv  39867