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  9253  djulepw  10298  infdjuabs  10310  xrsupss  13466  xrinfmss  13467  trclfv  15182  isumsplit  16038  ram0  17229  0mhm  19044  grpidssd  19255  gexdvds  19828  lsmdisj2  19926  mulgnn0di  20069  odadd1  20092  gsumval3  20151  telgsums  20237  dprdfadd  20266  rnglz  20417  rngrz  20418  zrrnghm  20818  orng0le1  21161  lspsneq  21430  rnglidl0  21539  rngqiprngimf1  21626  rngqiprngfulem5  21641  dsmmacl  22077  mplsubglem  22336  scmatmhm  22879  mdetuni0  22966  mndifsplit  22981  chfacfscmulgsum  23208  chfacfpmmulgsum  23212  alexsublem  24393  ovolunlem1  25848  mbfi1fseqlem4  26069  deg1lt  26445  deg1invg  26454  mon1pid  26502  cyclnumvtx  30418  sspz  31367  0lno  31422  pjhth  32025  pjhtheu  32026  pjpreeq  32030  opsqrlem1  32772  pfx1s2  33576  gsumwun  33707  0nellinds  33996  irredminply  34418  qqh1  34687  dnibndlem5  37526  relowlssretop  38478  mettrifi  38883  rngolz  39048  rngorz  39049  keridl  39158  lfl0f  40318  lkrlss  40344  lkrscss  40347  lkrin  40413  dihpN  42585  djh02  42662  lclkrlem1  42755  lclkr  42782  mon1psubm  44393  minregex  44727  clsneiel1  45300  stoweidlem22  47237  stoweidlem34  47249  sqwvfoura  47443  elaa2lem  47448  nzrneg1ne0  49532  onsetreclem2  51079