Theorem pm2.61ne 3010

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

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

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 2926

This theorem is referenced by:  pwdom  9046  cantnfle  9567  cantnflem1  9585  cantnf  9589  djulepw  10087  infmap2  10111  zornn0g  10399  ttukeylem6  10408  msqge0  11641  xrsupsslem  13209  xrinfmsslem  13210  fzoss1  13589  swrdcl  14552  pfxcl  14584  abs1m  15243  fsumcvg3  15636  bezoutlem4  16453  dvdssq  16478  lcmid  16520  pcdvdsb  16781  pcgcd1  16789  pc2dvds  16791  pcaddlem  16800  qexpz  16813  4sqlem19  16875  prmlem1a  17018  gsumwsubmcl  18711  gsumccat  18715  gsumwmhm  18719  cntzsdrg  20687  zringlpir  21374  psdmul  22051  mretopd  22977  ufildom1  23811  alexsublem  23929  nmolb2d  24604  nmoi  24614  nmoix  24615  ipcau2  25132  mdegcl  25972  ply1divex  26040  ig1pcl  26082  dgrmulc  26175  mulcxplem  26591  vmacl  27026  efvmacl  27028  vmalelog  27114  padicabv  27539  nmlnoubi  30740  nmblolbii  30743  blocnilem  30748  blocni  30749  ubthlem1  30814  nmbdoplbi  31968  cnlnadjlem7  32017  branmfn  32049  pjbdlni  32093  shatomistici  32305  segcon2  36083  lssats  38995  ps-1  39460  3atlem5  39470  lplnnle2at  39524  2llnm3N  39552  lvolnle3at  39565  4atex2  40060  cdlemd5  40185  cdleme21k  40321  cdlemg33b  40690  mapdrvallem2  41628  mapdhcl  41710  hdmapval3N  41821  hdmap10  41823  hdmaprnlem17N  41846  hdmap14lem2a  41850  hdmaplkr  41896  hgmapvv  41909  explt1d  42300  fiabv  42513