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  9247  djulepw  10230  infdjuabs  10242  xrsupss  13347  xrinfmss  13348  trclfv  15035  isumsplit  15872  ram0  17055  0mhm  18844  grpidssd  19046  gexdvds  19616  lsmdisj2  19714  mulgnn0di  19857  odadd1  19880  gsumval3  19939  telgsums  20025  dprdfadd  20054  rnglz  20182  rngrz  20183  zrrnghm  20552  lspsneq  21141  rnglidl0  21256  rngqiprngimf1  21327  rngqiprngfulem5  21342  dsmmacl  21778  mplsubglem  22036  scmatmhm  22555  mdetuni0  22642  mndifsplit  22657  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  alexsublem  24067  ovolunlem1  25545  mbfi1fseqlem4  25767  deg1lt  26150  deg1invg  26159  mon1pid  26207  sspz  30763  0lno  30818  pjhth  31421  pjhtheu  31422  pjpreeq  31426  opsqrlem1  32168  pfx1s2  32907  gsumwun  33050  orng0le1  33321  0nellinds  33377  irredminply  33721  qqh1  33947  dnibndlem5  36464  relowlssretop  37345  mettrifi  37743  rngolz  37908  rngorz  37909  keridl  38018  lfl0f  39050  lkrlss  39076  lkrscss  39079  lkrin  39145  dihpN  41318  djh02  41395  lclkrlem1  41488  lclkr  41515  mon1psubm  43187  minregex  43523  clsneiel1  44097  stoweidlem22  45977  stoweidlem34  45989  sqwvfoura  46183  elaa2lem  46188  nzrneg1ne0  48073  onsetreclem2  48936