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 397

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 206  df-an 398

This theorem is referenced by:  ssnnfiOLD  9170  php4  9213  djulepw  10187  infdjuabs  10201  xrsupss  13288  xrinfmss  13289  trclfv  14947  isumsplit  15786  ram0  16955  0mhm  18700  grpidssd  18899  gexdvds  19452  lsmdisj2  19550  mulgnn0di  19693  odadd1  19716  gsumval3  19775  telgsums  19861  dprdfadd  19890  ringlz  20107  ringrz  20108  lspsneq  20735  dsmmacl  21296  mplsubglem  21558  scmatmhm  22036  mdetuni0  22123  mndifsplit  22138  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  alexsublem  23548  ovolunlem1  25014  mbfi1fseqlem4  25236  deg1lt  25615  deg1invg  25624  sspz  29988  0lno  30043  pjhth  30646  pjhtheu  30647  pjpreeq  30651  opsqrlem1  31393  pfx1s2  32105  orng0le1  32430  0nellinds  32483  qqh1  32965  dnibndlem5  35358  relowlssretop  36244  mettrifi  36625  rngolz  36790  rngorz  36791  keridl  36900  lfl0f  37939  lkrlss  37965  lkrscss  37968  lkrin  38034  dihpN  40207  djh02  40284  lclkrlem1  40377  lclkr  40404  mon1pid  41947  mon1psubm  41948  minregex  42285  clsneiel1  42859  stoweidlem22  44738  stoweidlem34  44750  sqwvfoura  44944  elaa2lem  44949  nzrneg1ne0  46643  rnglz  46664  rngrz  46665  zrrnghm  46716  rnglidl0  46752  rngqiprngimf1  46785  rngqiprngfulem5  46800  onsetreclem2  47751