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  9129  djulepw  10094  infdjuabs  10106  xrsupss  13218  xrinfmss  13219  trclfv  14917  isumsplit  15757  ram0  16944  0mhm  18737  grpidssd  18939  gexdvds  19506  lsmdisj2  19604  mulgnn0di  19747  odadd1  19770  gsumval3  19829  telgsums  19915  dprdfadd  19944  rnglz  20093  rngrz  20094  zrrnghm  20461  orng0le1  20799  lspsneq  21069  rnglidl0  21176  rngqiprngimf1  21247  rngqiprngfulem5  21262  dsmmacl  21688  mplsubglem  21946  scmatmhm  22459  mdetuni0  22546  mndifsplit  22561  chfacfscmulgsum  22785  chfacfpmmulgsum  22789  alexsublem  23969  ovolunlem1  25435  mbfi1fseqlem4  25656  deg1lt  26039  deg1invg  26048  mon1pid  26096  sspz  30726  0lno  30781  pjhth  31384  pjhtheu  31385  pjpreeq  31389  opsqrlem1  32131  pfx1s2  32931  gsumwun  33056  0nellinds  33346  irredminply  33740  qqh1  34009  dnibndlem5  36537  relowlssretop  37418  mettrifi  37807  rngolz  37972  rngorz  37973  keridl  38082  lfl0f  39178  lkrlss  39204  lkrscss  39207  lkrin  39273  dihpN  41445  djh02  41522  lclkrlem1  41615  lclkr  41642  mon1psubm  43306  minregex  43641  clsneiel1  44215  stoweidlem22  46134  stoweidlem34  46146  sqwvfoura  46340  elaa2lem  46345  nzrneg1ne0  48344  onsetreclem2  49821