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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ≠ 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 197  df-an 385  df-ne 2933

This theorem is referenced by:  pwdom  8277  cantnfle  8741  cantnflem1  8759  cantnf  8763  cdalepw  9210  infmap2  9232  zornn0g  9519  ttukeylem6  9528  msqge0  10741  xrsupsslem  12330  xrinfmsslem  12331  fzoss1  12689  swrdcl  13618  abs1m  14274  fsumcvg3  14659  bezoutlem4  15461  gcdmultiplez  15472  dvdssq  15482  lcmid  15524  pcdvdsb  15775  pcgcd1  15783  pc2dvds  15785  pcaddlem  15794  qexpz  15807  4sqlem19  15869  prmlem1a  16015  gsumwsubmcl  17576  gsumccat  17579  gsumwmhm  17583  zringlpir  20039  mretopd  21098  ufildom1  21931  alexsublem  22049  nmolb2d  22723  nmoi  22733  nmoix  22734  ipcau2  23233  mdegcl  24028  ply1divex  24095  ig1pcl  24134  dgrmulc  24226  mulcxplem  24629  vmacl  25043  efvmacl  25045  vmalelog  25129  padicabv  25518  nmlnoubi  27960  nmblolbii  27963  blocnilem  27968  blocni  27969  ubthlem1  28035  nmbdoplbi  29192  cnlnadjlem7  29241  branmfn  29273  pjbdlni  29317  shatomistici  29529  segcon2  32518  lssats  34802  ps-1  35266  3atlem5  35276  lplnnle2at  35330  2llnm3N  35358  lvolnle3at  35371  4atex2  35866  cdlemd5  35992  cdleme21k  36128  cdlemg33b  36497  mapdrvallem2  37436  mapdhcl  37518  hdmapval3N  37632  hdmap10  37634  hdmaprnlem17N  37657  hdmap14lem2a  37661  hdmaplkr  37707  hgmapvv  37720  cntzsdrg  38274  pfxcl  41896