Theorem syl2anc2 593

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  php4  9167  djulepw  10139  infdjuabs  10151  xrsupss  13302  xrinfmss  13303  trclfv  15003  isumsplit  15846  ram0  17034  0mhm  18829  grpidssd  19034  gexdvds  19600  lsmdisj2  19698  mulgnn0di  19841  odadd1  19864  gsumval3  19923  telgsums  20009  dprdfadd  20038  rnglz  20187  rngrz  20188  zrrnghm  20558  orng0le1  20896  lspsneq  21165  rnglidl0  21272  rngqiprngimf1  21343  rngqiprngfulem5  21358  dsmmacl  21766  mplsubglem  22023  scmatmhm  22567  mdetuni0  22654  mndifsplit  22669  chfacfscmulgsum  22893  chfacfpmmulgsum  22897  alexsublem  24077  ovolunlem1  25532  mbfi1fseqlem4  25753  deg1lt  26130  deg1invg  26139  mon1pid  26187  sspz  30877  0lno  30932  pjhth  31535  pjhtheu  31536  pjpreeq  31540  opsqrlem1  32282  pfx1s2  33071  gsumwun  33210  0nellinds  33510  irredminply  33967  qqh1  34236  dnibndlem5  36868  relowlssretop  37805  mettrifi  38204  rngolz  38369  rngorz  38370  keridl  38479  lfl0f  39641  lkrlss  39667  lkrscss  39670  lkrin  39736  dihpN  41908  djh02  41985  lclkrlem1  42078  lclkr  42105  mon1psubm  43724  minregex  44058  clsneiel1  44632  stoweidlem22  46544  stoweidlem34  46556  sqwvfoura  46750  elaa2lem  46755  nzrneg1ne0  48800  onsetreclem2  50275