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 396

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 206  df-an 397

This theorem is referenced by:  ssnnfiOLD  9172  php4  9215  djulepw  10189  infdjuabs  10203  xrsupss  13290  xrinfmss  13291  trclfv  14949  isumsplit  15788  ram0  16957  0mhm  18702  grpidssd  18901  gexdvds  19454  lsmdisj2  19552  mulgnn0di  19695  odadd1  19718  gsumval3  19777  telgsums  19863  dprdfadd  19892  ringlz  20109  ringrz  20110  lspsneq  20741  dsmmacl  21302  mplsubglem  21564  scmatmhm  22043  mdetuni0  22130  mndifsplit  22145  chfacfscmulgsum  22369  chfacfpmmulgsum  22373  alexsublem  23555  ovolunlem1  25021  mbfi1fseqlem4  25243  deg1lt  25622  deg1invg  25631  sspz  30026  0lno  30081  pjhth  30684  pjhtheu  30685  pjpreeq  30689  opsqrlem1  31431  pfx1s2  32143  orng0le1  32471  0nellinds  32528  qqh1  33034  dnibndlem5  35444  relowlssretop  36330  mettrifi  36711  rngolz  36876  rngorz  36877  keridl  36986  lfl0f  38025  lkrlss  38051  lkrscss  38054  lkrin  38120  dihpN  40293  djh02  40370  lclkrlem1  40463  lclkr  40490  mon1pid  42029  mon1psubm  42030  minregex  42367  clsneiel1  42941  stoweidlem22  44817  stoweidlem34  44829  sqwvfoura  45023  elaa2lem  45028  nzrneg1ne0  46722  rnglz  46743  rngrz  46744  zrrnghm  46795  rnglidl0  46831  rngqiprngimf1  46864  rngqiprngfulem5  46879  onsetreclem2  47829