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  9207  djulepw  10198  infdjuabs  10210  xrsupss  13363  xrinfmss  13364  trclfv  15075  isumsplit  15931  ram0  17118  0mhm  18932  grpidssd  19143  gexdvds  19715  lsmdisj2  19813  mulgnn0di  19956  odadd1  19979  gsumval3  20038  telgsums  20124  dprdfadd  20153  rnglz  20304  rngrz  20305  zrrnghm  20702  orng0le1  21044  lspsneq  21313  rnglidl0  21422  rngqiprngimf1  21507  rngqiprngfulem5  21522  dsmmacl  21958  mplsubglem  22217  scmatmhm  22760  mdetuni0  22847  mndifsplit  22862  chfacfscmulgsum  23089  chfacfpmmulgsum  23093  alexsublem  24274  ovolunlem1  25729  mbfi1fseqlem4  25950  deg1lt  26327  deg1invg  26336  mon1pid  26384  cyclnumvtx  30268  sspz  31217  0lno  31272  pjhth  31875  pjhtheu  31876  pjpreeq  31880  opsqrlem1  32622  pfx1s2  33387  gsumwun  33518  0nellinds  33807  irredminply  34228  qqh1  34497  dnibndlem5  37181  relowlssretop  38119  mettrifi  38509  rngolz  38674  rngorz  38675  keridl  38784  lfl0f  39944  lkrlss  39970  lkrscss  39973  lkrin  40039  dihpN  42211  djh02  42288  lclkrlem1  42381  lclkr  42408  mon1psubm  44042  minregex  44376  clsneiel1  44950  stoweidlem22  46852  stoweidlem34  46864  sqwvfoura  47058  elaa2lem  47063  nzrneg1ne0  49147  onsetreclem2  50634