Theorem pm2.61ne 3043

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 249	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓))
4		pm2.61ne.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
5	4	expcom 418	. 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓))
6	3, 5	pm2.61ine 3041	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ≠ wne 2958

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 210  df-an 401  df-ne 2959

This theorem is referenced by:  pwdom  9113  cantnfle  9636  cantnflem1  9654  cantnf  9658  djulepw  10172  infmap2  10196  zornn0g  10484  ttukeylem6  10493  msqge0  11730  xrsupsslem  13328  xrinfmsslem  13329  fzoss1  13711  swrdcl  14679  pfxcl  14711  abs1m  15383  fsumcvg3  15776  bezoutlem4  16595  dvdssq  16620  lcmid  16662  pcdvdsb  16924  pcgcd1  16932  pc2dvds  16934  pcaddlem  16943  qexpz  16956  4sqlem19  17018  prmlem1a  17161  gsumwsubmcl  18891  gsumccat  18895  gsumwmhm  18899  cntzsdrg  20905  zringlpir  21617  psdmul  22329  mretopd  23249  ufildom1  24083  alexsublem  24201  nmolb2d  24875  nmoi  24885  nmoix  24886  ipcau2  25393  mdegcl  26226  ply1divex  26294  ig1pcl  26336  dgrmulc  26428  mulcxplem  26849  vmacl  27282  efvmacl  27284  vmalelog  27369  padicabv  27794  nmlnoubi  31148  nmblolbii  31151  blocnilem  31156  blocni  31157  ubthlem1  31222  nmbdoplbi  32376  cnlnadjlem7  32425  branmfn  32457  pjbdlni  32501  shatomistici  32713  segcon2  36597  lssats  39806  ps-1  40271  3atlem5  40281  lplnnle2at  40335  2llnm3N  40363  lvolnle3at  40376  4atex2  40871  cdlemd5  40996  cdleme21k  41132  cdlemg33b  41501  mapdrvallem2  42439  mapdhcl  42521  hdmapval3N  42632  hdmap10  42634  hdmaprnlem17N  42657  hdmap14lem2a  42661  hdmaplkr  42707  hgmapvv  42720  explt1d  43104  fiabv  43324