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  9174  djulepw  10146  infdjuabs  10158  xrsupss  13269  xrinfmss  13270  trclfv  14966  isumsplit  15806  ram0  16993  0mhm  18746  grpidssd  18948  gexdvds  19514  lsmdisj2  19612  mulgnn0di  19755  odadd1  19778  gsumval3  19837  telgsums  19923  dprdfadd  19952  rnglz  20074  rngrz  20075  zrrnghm  20445  lspsneq  21032  rnglidl0  21139  rngqiprngimf1  21210  rngqiprngfulem5  21225  dsmmacl  21650  mplsubglem  21908  scmatmhm  22421  mdetuni0  22508  mndifsplit  22523  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  alexsublem  23931  ovolunlem1  25398  mbfi1fseqlem4  25619  deg1lt  26002  deg1invg  26011  mon1pid  26059  sspz  30664  0lno  30719  pjhth  31322  pjhtheu  31323  pjpreeq  31327  opsqrlem1  32069  pfx1s2  32860  gsumwun  33005  orng0le1  33290  0nellinds  33341  irredminply  33706  qqh1  33975  dnibndlem5  36470  relowlssretop  37351  mettrifi  37751  rngolz  37916  rngorz  37917  keridl  38026  lfl0f  39062  lkrlss  39088  lkrscss  39091  lkrin  39157  dihpN  41330  djh02  41407  lclkrlem1  41500  lclkr  41527  mon1psubm  43188  minregex  43523  clsneiel1  44097  stoweidlem22  46020  stoweidlem34  46032  sqwvfoura  46226  elaa2lem  46231  nzrneg1ne0  48218  onsetreclem2  49695