Theorem pm2.61ne 3042

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1569   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-ne 2958

This theorem is used by:  pwdom  9115  cantnfle  9638  cantnflem1  9656  cantnf  9660  djulepw  10183  infmap2  10207  zornn0g  10495  ttukeylem6  10504  msqge0  11741  xrsupsslem  13339  xrinfmsslem  13340  fzoss1  13722  swrdcl  14690  pfxcl  14722  abs1m  15394  fsumcvg3  15787  bezoutlem4  16606  dvdssq  16631  lcmid  16673  pcdvdsb  16935  pcgcd1  16943  pc2dvds  16945  pcaddlem  16954  qexpz  16967  4sqlem19  17029  prmlem1a  17172  gsumwsubmcl  18902  gsumccat  18906  gsumwmhm  18910  cntzsdrg  20916  zringlpir  21628  psdmul  22340  mretopd  23260  ufildom1  24094  alexsublem  24212  nmolb2d  24886  nmoi  24896  nmoix  24897  ipcau2  25404  mdegcl  26237  ply1divex  26305  ig1pcl  26347  dgrmulc  26439  mulcxplem  26860  vmacl  27293  efvmacl  27295  vmalelog  27380  padicabv  27805  nmlnoubi  31159  nmblolbii  31162  blocnilem  31167  blocni  31168  ubthlem1  31233  nmbdoplbi  32387  cnlnadjlem7  32436  branmfn  32468  pjbdlni  32512  shatomistici  32724  segcon2  36605  lssats  39814  ps-1  40279  3atlem5  40289  lplnnle2at  40343  2llnm3N  40371  lvolnle3at  40384  4atex2  40879  cdlemd5  41004  cdleme21k  41140  cdlemg33b  41509  mapdrvallem2  42447  mapdhcl  42529  hdmapval3N  42640  hdmap10  42642  hdmaprnlem17N  42665  hdmap14lem2a  42669  hdmaplkr  42715  hgmapvv  42728  explt1d  43112  fiabv  43332