Theorem syl2anc2 586

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 585	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  9144  djulepw  10115  infdjuabs  10127  xrsupss  13261  xrinfmss  13262  trclfv  14962  isumsplit  15805  ram0  16993  0mhm  18787  grpidssd  18992  gexdvds  19559  lsmdisj2  19657  mulgnn0di  19800  odadd1  19823  gsumval3  19882  telgsums  19968  dprdfadd  19997  rnglz  20146  rngrz  20147  zrrnghm  20513  orng0le1  20851  lspsneq  21120  rnglidl0  21227  rngqiprngimf1  21298  rngqiprngfulem5  21313  dsmmacl  21721  mplsubglem  21977  scmatmhm  22499  mdetuni0  22586  mndifsplit  22601  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  alexsublem  24009  ovolunlem1  25464  mbfi1fseqlem4  25685  deg1lt  26062  deg1invg  26071  mon1pid  26119  sspz  30806  0lno  30861  pjhth  31464  pjhtheu  31465  pjpreeq  31469  opsqrlem1  32211  pfx1s2  32999  gsumwun  33137  0nellinds  33430  irredminply  33860  qqh1  34129  dnibndlem5  36742  relowlssretop  37679  mettrifi  38078  rngolz  38243  rngorz  38244  keridl  38353  lfl0f  39515  lkrlss  39541  lkrscss  39544  lkrin  39610  dihpN  41782  djh02  41859  lclkrlem1  41952  lclkr  41979  mon1psubm  43627  minregex  43961  clsneiel1  44535  stoweidlem22  46450  stoweidlem34  46462  sqwvfoura  46656  elaa2lem  46661  nzrneg1ne0  48700  onsetreclem2  50175