Theorem syl2anc2 597

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 18	. 2 ⊢ (𝜑 → 𝜒)
4		syl2anc2.3	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 3, 4	syl2anc 596	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  php4  9226  djulepw  10272  infdjuabs  10284  xrsupss  13440  xrinfmss  13441  trclfv  15154  isumsplit  16010  ram0  17201  0mhm  19016  grpidssd  19227  gexdvds  19799  lsmdisj2  19897  mulgnn0di  20040  odadd1  20063  gsumval3  20122  telgsums  20208  dprdfadd  20237  rnglz  20388  rngrz  20389  zrrnghm  20789  orng0le1  21132  lspsneq  21401  rnglidl0  21510  rngqiprngimf1  21597  rngqiprngfulem5  21612  dsmmacl  22048  mplsubglem  22307  scmatmhm  22850  mdetuni0  22937  mndifsplit  22952  chfacfscmulgsum  23179  chfacfpmmulgsum  23183  alexsublem  24364  ovolunlem1  25819  mbfi1fseqlem4  26040  deg1lt  26416  deg1invg  26425  mon1pid  26473  cyclnumvtx  30389  sspz  31338  0lno  31393  pjhth  31996  pjhtheu  31997  pjpreeq  32001  opsqrlem1  32743  pfx1s2  33549  gsumwun  33680  0nellinds  33969  irredminply  34391  qqh1  34660  dnibndlem5  37423  relowlssretop  38362  mettrifi  38767  rngolz  38932  rngorz  38933  keridl  39042  lfl0f  40202  lkrlss  40228  lkrscss  40231  lkrin  40297  dihpN  42469  djh02  42546  lclkrlem1  42639  lclkr  42666  mon1psubm  44277  minregex  44611  clsneiel1  45184  stoweidlem22  47108  stoweidlem34  47120  sqwvfoura  47314  elaa2lem  47319  nzrneg1ne0  49403  onsetreclem2  50875