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  9180  djulepw  10153  infdjuabs  10165  xrsupss  13276  xrinfmss  13277  trclfv  14973  isumsplit  15813  ram0  17000  0mhm  18753  grpidssd  18955  gexdvds  19521  lsmdisj2  19619  mulgnn0di  19762  odadd1  19785  gsumval3  19844  telgsums  19930  dprdfadd  19959  rnglz  20081  rngrz  20082  zrrnghm  20452  lspsneq  21039  rnglidl0  21146  rngqiprngimf1  21217  rngqiprngfulem5  21232  dsmmacl  21657  mplsubglem  21915  scmatmhm  22428  mdetuni0  22515  mndifsplit  22530  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  alexsublem  23938  ovolunlem1  25405  mbfi1fseqlem4  25626  deg1lt  26009  deg1invg  26018  mon1pid  26066  sspz  30671  0lno  30726  pjhth  31329  pjhtheu  31330  pjpreeq  31334  opsqrlem1  32076  pfx1s2  32867  gsumwun  33012  orng0le1  33297  0nellinds  33348  irredminply  33713  qqh1  33982  dnibndlem5  36477  relowlssretop  37358  mettrifi  37758  rngolz  37923  rngorz  37924  keridl  38033  lfl0f  39069  lkrlss  39095  lkrscss  39098  lkrin  39164  dihpN  41337  djh02  41414  lclkrlem1  41507  lclkr  41534  mon1psubm  43195  minregex  43530  clsneiel1  44104  stoweidlem22  46027  stoweidlem34  46039  sqwvfoura  46233  elaa2lem  46238  nzrneg1ne0  48222  onsetreclem2  49699