Theorem syl2anc2 591

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 590	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  php4  9141  djulepw  10113  infdjuabs  10125  xrsupss  13259  xrinfmss  13260  trclfv  14960  isumsplit  15803  ram0  16991  0mhm  18785  grpidssd  18990  gexdvds  19557  lsmdisj2  19655  mulgnn0di  19798  odadd1  19821  gsumval3  19880  telgsums  19966  dprdfadd  19995  rnglz  20144  rngrz  20145  zrrnghm  20515  orng0le1  20853  lspsneq  21122  rnglidl0  21229  rngqiprngimf1  21300  rngqiprngfulem5  21315  dsmmacl  21723  mplsubglem  21980  scmatmhm  22524  mdetuni0  22611  mndifsplit  22626  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  alexsublem  24034  ovolunlem1  25489  mbfi1fseqlem4  25710  deg1lt  26087  deg1invg  26096  mon1pid  26144  sspz  30831  0lno  30886  pjhth  31489  pjhtheu  31490  pjpreeq  31494  opsqrlem1  32236  pfx1s2  33025  gsumwun  33164  0nellinds  33460  irredminply  33907  qqh1  34176  dnibndlem5  36789  relowlssretop  37726  mettrifi  38125  rngolz  38290  rngorz  38291  keridl  38400  lfl0f  39562  lkrlss  39588  lkrscss  39591  lkrin  39657  dihpN  41829  djh02  41906  lclkrlem1  41999  lclkr  42026  mon1psubm  43645  minregex  43979  clsneiel1  44553  stoweidlem22  46466  stoweidlem34  46478  sqwvfoura  46672  elaa2lem  46677  nzrneg1ne0  48722  onsetreclem2  50197