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  9138  djulepw  10107  infdjuabs  10119  xrsupss  13228  xrinfmss  13229  trclfv  14927  isumsplit  15767  ram0  16954  0mhm  18748  grpidssd  18950  gexdvds  19517  lsmdisj2  19615  mulgnn0di  19758  odadd1  19781  gsumval3  19840  telgsums  19926  dprdfadd  19955  rnglz  20104  rngrz  20105  zrrnghm  20473  orng0le1  20811  lspsneq  21081  rnglidl0  21188  rngqiprngimf1  21259  rngqiprngfulem5  21274  dsmmacl  21700  mplsubglem  21958  scmatmhm  22482  mdetuni0  22569  mndifsplit  22584  chfacfscmulgsum  22808  chfacfpmmulgsum  22812  alexsublem  23992  ovolunlem1  25458  mbfi1fseqlem4  25679  deg1lt  26062  deg1invg  26071  mon1pid  26119  sspz  30793  0lno  30848  pjhth  31451  pjhtheu  31452  pjpreeq  31456  opsqrlem1  32198  pfx1s2  33002  gsumwun  33139  0nellinds  33432  irredminply  33854  qqh1  34123  dnibndlem5  36657  relowlssretop  37539  mettrifi  37929  rngolz  38094  rngorz  38095  keridl  38204  lfl0f  39366  lkrlss  39392  lkrscss  39395  lkrin  39461  dihpN  41633  djh02  41710  lclkrlem1  41803  lclkr  41830  mon1psubm  43477  minregex  43811  clsneiel1  44385  stoweidlem22  46302  stoweidlem34  46314  sqwvfoura  46508  elaa2lem  46513  nzrneg1ne0  48512  onsetreclem2  49987