Theorem syl2anc2 596

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 18	. 2 ⊢ (𝜑 → 𝜒)
4		syl2anc2.3	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 3, 4	syl2anc 595	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  php4  9193  djulepw  10175  infdjuabs  10187  xrsupss  13334  xrinfmss  13335  trclfv  15037  isumsplit  15894  ram0  17081  0mhm  18877  grpidssd  19081  gexdvds  19653  lsmdisj2  19751  mulgnn0di  19894  odadd1  19917  gsumval3  19976  telgsums  20062  dprdfadd  20091  rnglz  20242  rngrz  20243  zrrnghm  20620  orng0le1  20956  lspsneq  21225  rnglidl0  21334  rngqiprngimf1  21419  rngqiprngfulem5  21434  dsmmacl  21870  mplsubglem  22127  scmatmhm  22670  mdetuni0  22757  mndifsplit  22772  chfacfscmulgsum  22996  chfacfpmmulgsum  23000  alexsublem  24180  ovolunlem1  25635  mbfi1fseqlem4  25856  deg1lt  26233  deg1invg  26242  mon1pid  26290  cyclnumvtx  30115  sspz  31053  0lno  31108  pjhth  31711  pjhtheu  31712  pjpreeq  31716  opsqrlem1  32458  pfx1s2  33225  gsumwun  33362  0nellinds  33651  irredminply  34072  qqh1  34341  dnibndlem5  37037  relowlssretop  37975  mettrifi  38374  rngolz  38539  rngorz  38540  keridl  38649  lfl0f  39811  lkrlss  39837  lkrscss  39840  lkrin  39906  dihpN  42078  djh02  42155  lclkrlem1  42248  lclkr  42275  mon1psubm  43896  minregex  44230  clsneiel1  44804  stoweidlem22  46706  stoweidlem34  46718  sqwvfoura  46912  elaa2lem  46917  nzrneg1ne0  48962  onsetreclem2  50451