Theorem syl2anc2 585

Description: Double syllogism inference combined with contraction. (Contributed by BTernaryTau, 29-Sep-2023.)

Hypotheses

Ref	Expression
syl2anc2.1	⊢ (𝜑 → 𝜓)
syl2anc2.2	⊢ (𝜓 → 𝜒)
syl2anc2.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2anc2	⊢ (𝜑 → 𝜃)

Proof of Theorem syl2anc2

Step	Hyp	Ref	Expression
1		syl2anc2.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl2anc2.2	. . 3 ⊢ (𝜓 → 𝜒)
3	1, 2	syl 17	. 2 ⊢ (𝜑 → 𝜒)
4		syl2anc2.3	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 3, 4	syl2anc 584	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  php4  9134  djulepw  10106  infdjuabs  10118  xrsupss  13229  xrinfmss  13230  trclfv  14925  isumsplit  15765  ram0  16952  0mhm  18711  grpidssd  18913  gexdvds  19481  lsmdisj2  19579  mulgnn0di  19722  odadd1  19745  gsumval3  19804  telgsums  19890  dprdfadd  19919  rnglz  20068  rngrz  20069  zrrnghm  20439  orng0le1  20777  lspsneq  21047  rnglidl0  21154  rngqiprngimf1  21225  rngqiprngfulem5  21240  dsmmacl  21666  mplsubglem  21924  scmatmhm  22437  mdetuni0  22524  mndifsplit  22539  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  alexsublem  23947  ovolunlem1  25414  mbfi1fseqlem4  25635  deg1lt  26018  deg1invg  26027  mon1pid  26075  sspz  30697  0lno  30752  pjhth  31355  pjhtheu  31356  pjpreeq  31360  opsqrlem1  32102  pfx1s2  32893  gsumwun  33031  0nellinds  33317  irredminply  33682  qqh1  33951  dnibndlem5  36455  relowlssretop  37336  mettrifi  37736  rngolz  37901  rngorz  37902  keridl  38011  lfl0f  39047  lkrlss  39073  lkrscss  39076  lkrin  39142  dihpN  41315  djh02  41392  lclkrlem1  41485  lclkr  41512  mon1psubm  43172  minregex  43507  clsneiel1  44081  stoweidlem22  46004  stoweidlem34  46016  sqwvfoura  46210  elaa2lem  46215  nzrneg1ne0  48202  onsetreclem2  49679