Theorem syl2anc2 597

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  php4  9203  djulepw  10243  infdjuabs  10255  xrsupss  13409  xrinfmss  13410  trclfv  15121  isumsplit  15977  ram0  17162  0mhm  18977  grpidssd  19188  gexdvds  19760  lsmdisj2  19858  mulgnn0di  20001  odadd1  20024  gsumval3  20083  telgsums  20169  dprdfadd  20198  rnglz  20349  rngrz  20350  zrrnghm  20750  orng0le1  21093  lspsneq  21362  rnglidl0  21471  rngqiprngimf1  21558  rngqiprngfulem5  21573  dsmmacl  22009  mplsubglem  22268  scmatmhm  22811  mdetuni0  22898  mndifsplit  22913  chfacfscmulgsum  23140  chfacfpmmulgsum  23144  alexsublem  24325  ovolunlem1  25780  mbfi1fseqlem4  26001  deg1lt  26377  deg1invg  26386  mon1pid  26434  cyclnumvtx  30322  sspz  31271  0lno  31326  pjhth  31929  pjhtheu  31930  pjpreeq  31934  opsqrlem1  32676  pfx1s2  33440  gsumwun  33571  0nellinds  33860  irredminply  34282  qqh1  34551  dnibndlem5  37270  relowlssretop  38206  mettrifi  38611  rngolz  38776  rngorz  38777  keridl  38886  lfl0f  40046  lkrlss  40072  lkrscss  40075  lkrin  40141  dihpN  42313  djh02  42390  lclkrlem1  42483  lclkr  42510  mon1psubm  44144  minregex  44478  clsneiel1  45052  stoweidlem22  46954  stoweidlem34  46966  sqwvfoura  47160  elaa2lem  47165  nzrneg1ne0  49249  onsetreclem2  50721