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  9250  djulepw  10233  infdjuabs  10245  xrsupss  13351  xrinfmss  13352  trclfv  15039  isumsplit  15876  ram0  17060  0mhm  18832  grpidssd  19034  gexdvds  19602  lsmdisj2  19700  mulgnn0di  19843  odadd1  19866  gsumval3  19925  telgsums  20011  dprdfadd  20040  rnglz  20162  rngrz  20163  zrrnghm  20536  lspsneq  21124  rnglidl0  21239  rngqiprngimf1  21310  rngqiprngfulem5  21325  dsmmacl  21761  mplsubglem  22019  scmatmhm  22540  mdetuni0  22627  mndifsplit  22642  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  alexsublem  24052  ovolunlem1  25532  mbfi1fseqlem4  25753  deg1lt  26136  deg1invg  26145  mon1pid  26193  sspz  30754  0lno  30809  pjhth  31412  pjhtheu  31413  pjpreeq  31417  opsqrlem1  32159  pfx1s2  32923  gsumwun  33068  orng0le1  33342  0nellinds  33398  irredminply  33757  qqh1  33986  dnibndlem5  36483  relowlssretop  37364  mettrifi  37764  rngolz  37929  rngorz  37930  keridl  38039  lfl0f  39070  lkrlss  39096  lkrscss  39099  lkrin  39165  dihpN  41338  djh02  41415  lclkrlem1  41508  lclkr  41535  mon1psubm  43211  minregex  43547  clsneiel1  44121  stoweidlem22  46037  stoweidlem34  46049  sqwvfoura  46243  elaa2lem  46248  nzrneg1ne0  48146  onsetreclem2  49225