Theorem pm2.61ne 3027

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

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

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 2941

This theorem is referenced by:  pwdom  9169  cantnfle  9711  cantnflem1  9729  cantnf  9733  djulepw  10233  infmap2  10257  zornn0g  10545  ttukeylem6  10554  msqge0  11784  xrsupsslem  13349  xrinfmsslem  13350  fzoss1  13726  swrdcl  14683  pfxcl  14715  abs1m  15374  fsumcvg3  15765  bezoutlem4  16579  dvdssq  16604  lcmid  16646  pcdvdsb  16907  pcgcd1  16915  pc2dvds  16917  pcaddlem  16926  qexpz  16939  4sqlem19  17001  prmlem1a  17144  gsumwsubmcl  18850  gsumccat  18854  gsumwmhm  18858  cntzsdrg  20803  zringlpir  21478  psdmul  22170  mretopd  23100  ufildom1  23934  alexsublem  24052  nmolb2d  24739  nmoi  24749  nmoix  24750  ipcau2  25268  mdegcl  26108  ply1divex  26176  ig1pcl  26218  dgrmulc  26311  mulcxplem  26726  vmacl  27161  efvmacl  27163  vmalelog  27249  padicabv  27674  nmlnoubi  30815  nmblolbii  30818  blocnilem  30823  blocni  30824  ubthlem1  30889  nmbdoplbi  32043  cnlnadjlem7  32092  branmfn  32124  pjbdlni  32168  shatomistici  32380  segcon2  36106  lssats  39013  ps-1  39479  3atlem5  39489  lplnnle2at  39543  2llnm3N  39571  lvolnle3at  39584  4atex2  40079  cdlemd5  40204  cdleme21k  40340  cdlemg33b  40709  mapdrvallem2  41647  mapdhcl  41729  hdmapval3N  41840  hdmap10  41842  hdmaprnlem17N  41865  hdmap14lem2a  41869  hdmaplkr  41915  hgmapvv  41928  explt1d  42358  fiabv  42546