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 207  df-an 396

This theorem is referenced by:  ssnnfiOLD  9236  php4  9276  djulepw  10262  infdjuabs  10274  xrsupss  13371  xrinfmss  13372  trclfv  15049  isumsplit  15888  ram0  17069  0mhm  18854  grpidssd  19056  gexdvds  19626  lsmdisj2  19724  mulgnn0di  19867  odadd1  19890  gsumval3  19949  telgsums  20035  dprdfadd  20064  rnglz  20192  rngrz  20193  zrrnghm  20562  lspsneq  21147  rnglidl0  21262  rngqiprngimf1  21333  rngqiprngfulem5  21348  dsmmacl  21784  mplsubglem  22042  scmatmhm  22561  mdetuni0  22648  mndifsplit  22663  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  alexsublem  24073  ovolunlem1  25551  mbfi1fseqlem4  25773  deg1lt  26156  deg1invg  26165  mon1pid  26213  sspz  30767  0lno  30822  pjhth  31425  pjhtheu  31426  pjpreeq  31430  opsqrlem1  32172  pfx1s2  32905  orng0le1  33307  0nellinds  33363  irredminply  33707  qqh1  33931  dnibndlem5  36448  relowlssretop  37329  mettrifi  37717  rngolz  37882  rngorz  37883  keridl  37992  lfl0f  39025  lkrlss  39051  lkrscss  39054  lkrin  39120  dihpN  41293  djh02  41370  lclkrlem1  41463  lclkr  41490  mon1psubm  43160  minregex  43496  clsneiel1  44070  stoweidlem22  45943  stoweidlem34  45955  sqwvfoura  46149  elaa2lem  46154  nzrneg1ne0  47953  onsetreclem2  48798