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  9114  djulepw  10076  infdjuabs  10088  xrsupss  13200  xrinfmss  13201  trclfv  14899  isumsplit  15739  ram0  16926  0mhm  18719  grpidssd  18921  gexdvds  19489  lsmdisj2  19587  mulgnn0di  19730  odadd1  19753  gsumval3  19812  telgsums  19898  dprdfadd  19927  rnglz  20076  rngrz  20077  zrrnghm  20444  orng0le1  20782  lspsneq  21052  rnglidl0  21159  rngqiprngimf1  21230  rngqiprngfulem5  21245  dsmmacl  21671  mplsubglem  21929  scmatmhm  22442  mdetuni0  22529  mndifsplit  22544  chfacfscmulgsum  22768  chfacfpmmulgsum  22772  alexsublem  23952  ovolunlem1  25418  mbfi1fseqlem4  25639  deg1lt  26022  deg1invg  26031  mon1pid  26079  sspz  30705  0lno  30760  pjhth  31363  pjhtheu  31364  pjpreeq  31368  opsqrlem1  32110  pfx1s2  32910  gsumwun  33035  0nellinds  33325  irredminply  33719  qqh1  33988  dnibndlem5  36495  relowlssretop  37376  mettrifi  37776  rngolz  37941  rngorz  37942  keridl  38051  lfl0f  39087  lkrlss  39113  lkrscss  39116  lkrin  39182  dihpN  41354  djh02  41431  lclkrlem1  41524  lclkr  41551  mon1psubm  43211  minregex  43546  clsneiel1  44120  stoweidlem22  46039  stoweidlem34  46051  sqwvfoura  46245  elaa2lem  46250  nzrneg1ne0  48240  onsetreclem2  49717