Theorem syl2anc2 587

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  php4  8704  ssnnfi  8737  djulepw  9618  infdjuabs  9628  xrsupss  12703  xrinfmss  12704  trclfv  14360  isumsplit  15195  ram0  16358  0mhm  17984  grpidssd  18175  gexdvds  18709  lsmdisj2  18808  mulgnn0di  18946  odadd1  18968  gsumval3  19027  telgsums  19113  dprdfadd  19142  ringlz  19337  ringrz  19338  lspsneq  19894  mplsubglem  20214  dsmmacl  20885  scmatmhm  21143  mdetuni0  21230  mndifsplit  21245  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  alexsublem  22652  ovolunlem1  24098  mbfi1fseqlem4  24319  deg1lt  24691  deg1invg  24700  sspz  28512  0lno  28567  pjhth  29170  pjhtheu  29171  pjpreeq  29175  opsqrlem1  29917  pfx1s2  30615  orng0le1  30885  0nellinds  30935  qqh1  31226  dnibndlem5  33821  relowlssretop  34647  mettrifi  35047  rngolz  35215  rngorz  35216  keridl  35325  lfl0f  36220  lkrlss  36246  lkrscss  36249  lkrin  36315  dihpN  38487  djh02  38564  lclkrlem1  38657  lclkr  38684  mon1pid  39854  mon1psubm  39855  clsneiel1  40507  disjinfi  41503  stoweidlem22  42356  stoweidlem34  42368  sqwvfoura  42562  elaa2lem  42567  nzrneg1ne0  44189  rnglz  44204  zrrnghm  44237  onsetreclem2  44857