Theorem syl2anc2 586

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 585	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:  php4  9135  djulepw  10104  infdjuabs  10116  xrsupss  13250  xrinfmss  13251  trclfv  14951  isumsplit  15794  ram0  16982  0mhm  18776  grpidssd  18981  gexdvds  19548  lsmdisj2  19646  mulgnn0di  19789  odadd1  19812  gsumval3  19871  telgsums  19957  dprdfadd  19986  rnglz  20135  rngrz  20136  zrrnghm  20502  orng0le1  20840  lspsneq  21110  rnglidl0  21217  rngqiprngimf1  21288  rngqiprngfulem5  21303  dsmmacl  21729  mplsubglem  21986  scmatmhm  22508  mdetuni0  22595  mndifsplit  22610  chfacfscmulgsum  22834  chfacfpmmulgsum  22838  alexsublem  24018  ovolunlem1  25473  mbfi1fseqlem4  25694  deg1lt  26074  deg1invg  26083  mon1pid  26131  sspz  30826  0lno  30881  pjhth  31484  pjhtheu  31485  pjpreeq  31489  opsqrlem1  32231  pfx1s2  33019  gsumwun  33157  0nellinds  33450  irredminply  33881  qqh1  34150  dnibndlem5  36755  relowlssretop  37690  mettrifi  38089  rngolz  38254  rngorz  38255  keridl  38364  lfl0f  39526  lkrlss  39552  lkrscss  39555  lkrin  39621  dihpN  41793  djh02  41870  lclkrlem1  41963  lclkr  41990  mon1psubm  43642  minregex  43976  clsneiel1  44550  stoweidlem22  46465  stoweidlem34  46477  sqwvfoura  46671  elaa2lem  46676  nzrneg1ne0  48703  onsetreclem2  50178