Theorem syl2anc2 588

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 587	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  php4  8740  ssnnfi  8753  djulepw  9666  infdjuabs  9680  xrsupss  12757  xrinfmss  12758  trclfv  14421  isumsplit  15257  ram0  16428  0mhm  18065  grpidssd  18257  gexdvds  18791  lsmdisj2  18890  mulgnn0di  19029  odadd1  19051  gsumval3  19110  telgsums  19196  dprdfadd  19225  ringlz  19423  ringrz  19424  lspsneq  19977  dsmmacl  20521  mplsubglem  20779  scmatmhm  21249  mdetuni0  21336  mndifsplit  21351  chfacfscmulgsum  21575  chfacfpmmulgsum  21579  alexsublem  22759  ovolunlem1  24212  mbfi1fseqlem4  24433  deg1lt  24812  deg1invg  24821  sspz  28632  0lno  28687  pjhth  29290  pjhtheu  29291  pjpreeq  29295  opsqrlem1  30037  pfx1s2  30751  orng0le1  31051  0nellinds  31101  qqh1  31468  dnibndlem5  34247  relowlssretop  35096  mettrifi  35511  rngolz  35676  rngorz  35677  keridl  35786  lfl0f  36681  lkrlss  36707  lkrscss  36710  lkrin  36776  dihpN  38948  djh02  39025  lclkrlem1  39118  lclkr  39145  mon1pid  40568  mon1psubm  40569  clsneiel1  41230  stoweidlem22  43076  stoweidlem34  43088  sqwvfoura  43282  elaa2lem  43287  nzrneg1ne0  44920  rnglz  44935  zrrnghm  44968  onsetreclem2  45733