Theorem syl2anc2 585

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 584	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  9224  djulepw  10207  infdjuabs  10219  xrsupss  13325  xrinfmss  13326  trclfv  15019  isumsplit  15856  ram0  17042  0mhm  18797  grpidssd  18999  gexdvds  19565  lsmdisj2  19663  mulgnn0di  19806  odadd1  19829  gsumval3  19888  telgsums  19974  dprdfadd  20003  rnglz  20125  rngrz  20126  zrrnghm  20496  lspsneq  21083  rnglidl0  21190  rngqiprngimf1  21261  rngqiprngfulem5  21276  dsmmacl  21701  mplsubglem  21959  scmatmhm  22472  mdetuni0  22559  mndifsplit  22574  chfacfscmulgsum  22798  chfacfpmmulgsum  22802  alexsublem  23982  ovolunlem1  25450  mbfi1fseqlem4  25671  deg1lt  26054  deg1invg  26063  mon1pid  26111  sspz  30716  0lno  30771  pjhth  31374  pjhtheu  31375  pjpreeq  31379  opsqrlem1  32121  pfx1s2  32914  gsumwun  33059  orng0le1  33334  0nellinds  33385  irredminply  33750  qqh1  34016  dnibndlem5  36500  relowlssretop  37381  mettrifi  37781  rngolz  37946  rngorz  37947  keridl  38056  lfl0f  39087  lkrlss  39113  lkrscss  39116  lkrin  39182  dihpN  41355  djh02  41432  lclkrlem1  41525  lclkr  41552  mon1psubm  43223  minregex  43558  clsneiel1  44132  stoweidlem22  46051  stoweidlem34  46063  sqwvfoura  46257  elaa2lem  46262  nzrneg1ne0  48205  onsetreclem2  49570