Theorem syl2anc2 596

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 595	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

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 401

This theorem is used by:  php4  9192  djulepw  10183  infdjuabs  10195  xrsupss  13341  xrinfmss  13342  trclfv  15044  isumsplit  15901  ram0  17088  0mhm  18884  grpidssd  19088  gexdvds  19660  lsmdisj2  19758  mulgnn0di  19901  odadd1  19924  gsumval3  19983  telgsums  20069  dprdfadd  20098  rnglz  20249  rngrz  20250  zrrnghm  20646  orng0le1  20988  lspsneq  21257  rnglidl0  21366  rngqiprngimf1  21451  rngqiprngfulem5  21466  dsmmacl  21902  mplsubglem  22159  scmatmhm  22702  mdetuni0  22789  mndifsplit  22804  chfacfscmulgsum  23028  chfacfpmmulgsum  23032  alexsublem  24212  ovolunlem1  25667  mbfi1fseqlem4  25888  deg1lt  26265  deg1invg  26274  mon1pid  26322  cyclnumvtx  30160  sspz  31098  0lno  31153  pjhth  31756  pjhtheu  31757  pjpreeq  31761  opsqrlem1  32503  pfx1s2  33270  gsumwun  33405  0nellinds  33694  irredminply  34115  qqh1  34384  dnibndlem5  37099  relowlssretop  38037  mettrifi  38436  rngolz  38601  rngorz  38602  keridl  38711  lfl0f  39871  lkrlss  39897  lkrscss  39900  lkrin  39966  dihpN  42138  djh02  42215  lclkrlem1  42308  lclkr  42335  mon1psubm  43954  minregex  44288  clsneiel1  44862  stoweidlem22  46764  stoweidlem34  46776  sqwvfoura  46970  elaa2lem  46975  nzrneg1ne0  49023  onsetreclem2  50512