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  9146  djulepw  10115  infdjuabs  10127  xrsupss  13236  xrinfmss  13237  trclfv  14935  isumsplit  15775  ram0  16962  0mhm  18756  grpidssd  18958  gexdvds  19525  lsmdisj2  19623  mulgnn0di  19766  odadd1  19789  gsumval3  19848  telgsums  19934  dprdfadd  19963  rnglz  20112  rngrz  20113  zrrnghm  20481  orng0le1  20819  lspsneq  21089  rnglidl0  21196  rngqiprngimf1  21267  rngqiprngfulem5  21282  dsmmacl  21708  mplsubglem  21966  scmatmhm  22490  mdetuni0  22577  mndifsplit  22592  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  alexsublem  24000  ovolunlem1  25466  mbfi1fseqlem4  25687  deg1lt  26070  deg1invg  26079  mon1pid  26127  sspz  30822  0lno  30877  pjhth  31480  pjhtheu  31481  pjpreeq  31485  opsqrlem1  32227  pfx1s2  33031  gsumwun  33169  0nellinds  33462  irredminply  33893  qqh1  34162  dnibndlem5  36701  relowlssretop  37607  mettrifi  37997  rngolz  38162  rngorz  38163  keridl  38272  lfl0f  39434  lkrlss  39460  lkrscss  39463  lkrin  39529  dihpN  41701  djh02  41778  lclkrlem1  41871  lclkr  41898  mon1psubm  43545  minregex  43879  clsneiel1  44453  stoweidlem22  46369  stoweidlem34  46381  sqwvfoura  46575  elaa2lem  46580  nzrneg1ne0  48579  onsetreclem2  50054