Theorem pm2.61ne 3017

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

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

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 2933

This theorem is referenced by:  pwdom  9141  cantnfle  9683  cantnflem1  9701  cantnf  9705  djulepw  10205  infmap2  10229  zornn0g  10517  ttukeylem6  10526  msqge0  11756  xrsupsslem  13321  xrinfmsslem  13322  fzoss1  13701  swrdcl  14661  pfxcl  14693  abs1m  15352  fsumcvg3  15743  bezoutlem4  16559  dvdssq  16584  lcmid  16626  pcdvdsb  16887  pcgcd1  16895  pc2dvds  16897  pcaddlem  16906  qexpz  16919  4sqlem19  16981  prmlem1a  17124  gsumwsubmcl  18813  gsumccat  18817  gsumwmhm  18821  cntzsdrg  20760  zringlpir  21426  psdmul  22102  mretopd  23028  ufildom1  23862  alexsublem  23980  nmolb2d  24655  nmoi  24665  nmoix  24666  ipcau2  25184  mdegcl  26024  ply1divex  26092  ig1pcl  26134  dgrmulc  26227  mulcxplem  26643  vmacl  27078  efvmacl  27080  vmalelog  27166  padicabv  27591  nmlnoubi  30723  nmblolbii  30726  blocnilem  30731  blocni  30732  ubthlem1  30797  nmbdoplbi  31951  cnlnadjlem7  32000  branmfn  32032  pjbdlni  32076  shatomistici  32288  segcon2  36069  lssats  38976  ps-1  39442  3atlem5  39452  lplnnle2at  39506  2llnm3N  39534  lvolnle3at  39547  4atex2  40042  cdlemd5  40167  cdleme21k  40303  cdlemg33b  40672  mapdrvallem2  41610  mapdhcl  41692  hdmapval3N  41803  hdmap10  41805  hdmaprnlem17N  41828  hdmap14lem2a  41832  hdmaplkr  41878  hgmapvv  41891  explt1d  42319  fiabv  42506