Theorem syl2anc2 584

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 583	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 206  df-an 396

This theorem is referenced by:  php4  8900  ssnnfiOLD  8915  djulepw  9879  infdjuabs  9893  xrsupss  12972  xrinfmss  12973  trclfv  14639  isumsplit  15480  ram0  16651  0mhm  18373  grpidssd  18566  gexdvds  19104  lsmdisj2  19203  mulgnn0di  19342  odadd1  19364  gsumval3  19423  telgsums  19509  dprdfadd  19538  ringlz  19741  ringrz  19742  lspsneq  20299  dsmmacl  20858  mplsubglem  21115  scmatmhm  21591  mdetuni0  21678  mndifsplit  21693  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  alexsublem  23103  ovolunlem1  24566  mbfi1fseqlem4  24788  deg1lt  25167  deg1invg  25176  sspz  28998  0lno  29053  pjhth  29656  pjhtheu  29657  pjpreeq  29661  opsqrlem1  30403  pfx1s2  31115  orng0le1  31413  0nellinds  31468  qqh1  31835  dnibndlem5  34589  relowlssretop  35461  mettrifi  35842  rngolz  36007  rngorz  36008  keridl  36117  lfl0f  37010  lkrlss  37036  lkrscss  37039  lkrin  37105  dihpN  39277  djh02  39354  lclkrlem1  39447  lclkr  39474  mon1pid  40946  mon1psubm  40947  clsneiel1  41607  stoweidlem22  43453  stoweidlem34  43465  sqwvfoura  43659  elaa2lem  43664  nzrneg1ne0  45315  rnglz  45330  zrrnghm  45363  onsetreclem2  46297