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  8962  php4  9005  djulepw  9957  infdjuabs  9971  xrsupss  13052  xrinfmss  13053  trclfv  14720  isumsplit  15561  ram0  16732  0mhm  18467  grpidssd  18660  gexdvds  19198  lsmdisj2  19297  mulgnn0di  19436  odadd1  19458  gsumval3  19517  telgsums  19603  dprdfadd  19632  ringlz  19835  ringrz  19836  lspsneq  20393  dsmmacl  20957  mplsubglem  21214  scmatmhm  21692  mdetuni0  21779  mndifsplit  21794  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  alexsublem  23204  ovolunlem1  24670  mbfi1fseqlem4  24892  deg1lt  25271  deg1invg  25280  sspz  29106  0lno  29161  pjhth  29764  pjhtheu  29765  pjpreeq  29769  opsqrlem1  30511  pfx1s2  31222  orng0le1  31520  0nellinds  31575  qqh1  31944  dnibndlem5  34671  relowlssretop  35543  mettrifi  35924  rngolz  36089  rngorz  36090  keridl  36199  lfl0f  37090  lkrlss  37116  lkrscss  37119  lkrin  37185  dihpN  39357  djh02  39434  lclkrlem1  39527  lclkr  39554  mon1pid  41037  mon1psubm  41038  minregex  41148  clsneiel1  41725  stoweidlem22  43570  stoweidlem34  43582  sqwvfoura  43776  elaa2lem  43781  nzrneg1ne0  45438  rnglz  45453  zrrnghm  45486  onsetreclem2  46422