Theorem pm2.61ne 3049

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ≠ wne 2964

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 210  df-an 401  df-ne 2965

This theorem is referenced by:  pwdom  9117  cantnfle  9640  cantnflem1  9658  cantnf  9662  djulepw  10176  infmap2  10200  zornn0g  10489  ttukeylem6  10498  msqge0  11735  xrsupsslem  13333  xrinfmsslem  13334  fzoss1  13715  swrdcl  14683  pfxcl  14715  abs1m  15387  fsumcvg3  15780  bezoutlem4  16600  dvdssq  16625  lcmid  16667  pcdvdsb  16929  pcgcd1  16937  pc2dvds  16939  pcaddlem  16948  qexpz  16961  4sqlem19  17023  prmlem1a  17166  gsumwsubmcl  18896  gsumccat  18900  gsumwmhm  18904  cntzsdrg  20883  zringlpir  21586  psdmul  22298  mretopd  23218  ufildom1  24052  alexsublem  24170  nmolb2d  24844  nmoi  24854  nmoix  24855  ipcau2  25362  mdegcl  26195  ply1divex  26263  ig1pcl  26305  dgrmulc  26397  mulcxplem  26815  vmacl  27248  efvmacl  27250  vmalelog  27335  padicabv  27760  nmlnoubi  31089  nmblolbii  31092  blocnilem  31097  blocni  31098  ubthlem1  31163  nmbdoplbi  32317  cnlnadjlem7  32366  branmfn  32398  pjbdlni  32442  shatomistici  32654  segcon2  36496  lssats  39676  ps-1  40141  3atlem5  40151  lplnnle2at  40205  2llnm3N  40233  lvolnle3at  40246  4atex2  40741  cdlemd5  40866  cdleme21k  41002  cdlemg33b  41371  mapdrvallem2  42309  mapdhcl  42391  hdmapval3N  42502  hdmap10  42504  hdmaprnlem17N  42527  hdmap14lem2a  42531  hdmaplkr  42577  hgmapvv  42590  explt1d  42974  fiabv  43196