Theorem pm2.61ne 3011

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

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

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 2927

This theorem is referenced by:  pwdom  9098  cantnfle  9630  cantnflem1  9648  cantnf  9652  djulepw  10152  infmap2  10176  zornn0g  10464  ttukeylem6  10473  msqge0  11705  xrsupsslem  13273  xrinfmsslem  13274  fzoss1  13653  swrdcl  14616  pfxcl  14648  abs1m  15308  fsumcvg3  15701  bezoutlem4  16518  dvdssq  16543  lcmid  16585  pcdvdsb  16846  pcgcd1  16854  pc2dvds  16856  pcaddlem  16865  qexpz  16878  4sqlem19  16940  prmlem1a  17083  gsumwsubmcl  18770  gsumccat  18774  gsumwmhm  18778  cntzsdrg  20717  zringlpir  21383  psdmul  22059  mretopd  22985  ufildom1  23819  alexsublem  23937  nmolb2d  24612  nmoi  24622  nmoix  24623  ipcau2  25140  mdegcl  25980  ply1divex  26048  ig1pcl  26090  dgrmulc  26183  mulcxplem  26599  vmacl  27034  efvmacl  27036  vmalelog  27122  padicabv  27547  nmlnoubi  30731  nmblolbii  30734  blocnilem  30739  blocni  30740  ubthlem1  30805  nmbdoplbi  31959  cnlnadjlem7  32008  branmfn  32040  pjbdlni  32084  shatomistici  32296  segcon2  36088  lssats  39000  ps-1  39466  3atlem5  39476  lplnnle2at  39530  2llnm3N  39558  lvolnle3at  39571  4atex2  40066  cdlemd5  40191  cdleme21k  40327  cdlemg33b  40696  mapdrvallem2  41634  mapdhcl  41716  hdmapval3N  41827  hdmap10  41829  hdmaprnlem17N  41852  hdmap14lem2a  41856  hdmaplkr  41902  hgmapvv  41915  explt1d  42306  fiabv  42517