Theorem pm2.61ne 3024

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

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

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 2938

This theorem is referenced by:  pwdom  9167  cantnfle  9708  cantnflem1  9726  cantnf  9730  djulepw  10230  infmap2  10254  zornn0g  10542  ttukeylem6  10551  msqge0  11781  xrsupsslem  13345  xrinfmsslem  13346  fzoss1  13722  swrdcl  14679  pfxcl  14711  abs1m  15370  fsumcvg3  15761  bezoutlem4  16575  dvdssq  16600  lcmid  16642  pcdvdsb  16902  pcgcd1  16910  pc2dvds  16912  pcaddlem  16921  qexpz  16934  4sqlem19  16996  prmlem1a  17140  gsumwsubmcl  18862  gsumccat  18866  gsumwmhm  18870  cntzsdrg  20819  zringlpir  21495  psdmul  22187  mretopd  23115  ufildom1  23949  alexsublem  24067  nmolb2d  24754  nmoi  24764  nmoix  24765  ipcau2  25281  mdegcl  26122  ply1divex  26190  ig1pcl  26232  dgrmulc  26325  mulcxplem  26740  vmacl  27175  efvmacl  27177  vmalelog  27263  padicabv  27688  nmlnoubi  30824  nmblolbii  30827  blocnilem  30832  blocni  30833  ubthlem1  30898  nmbdoplbi  32052  cnlnadjlem7  32101  branmfn  32133  pjbdlni  32177  shatomistici  32389  segcon2  36086  lssats  38993  ps-1  39459  3atlem5  39469  lplnnle2at  39523  2llnm3N  39551  lvolnle3at  39564  4atex2  40059  cdlemd5  40184  cdleme21k  40320  cdlemg33b  40689  mapdrvallem2  41627  mapdhcl  41709  hdmapval3N  41820  hdmap10  41822  hdmaprnlem17N  41845  hdmap14lem2a  41849  hdmaplkr  41895  hgmapvv  41908  explt1d  42336  fiabv  42522