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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  php4  9182  djulepw  10164  infdjuabs  10176  xrsupss  13326  xrinfmss  13327  trclfv  15027  isumsplit  15884  ram0  17072  0mhm  18868  grpidssd  19073  gexdvds  19645  lsmdisj2  19743  mulgnn0di  19886  odadd1  19909  gsumval3  19968  telgsums  20054  dprdfadd  20083  rnglz  20234  rngrz  20235  zrrnghm  20612  orng0le1  20946  lspsneq  21215  rnglidl0  21324  rngqiprngimf1  21402  rngqiprngfulem5  21417  dsmmacl  21851  mplsubglem  22108  scmatmhm  22652  mdetuni0  22739  mndifsplit  22754  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  alexsublem  24162  ovolunlem1  25617  mbfi1fseqlem4  25838  deg1lt  26215  deg1invg  26224  mon1pid  26272  sspz  30996  0lno  31051  pjhth  31654  pjhtheu  31655  pjpreeq  31659  opsqrlem1  32401  pfx1s2  33172  gsumwun  33309  0nellinds  33600  irredminply  34023  qqh1  34292  dnibndlem5  36933  relowlssretop  37869  mettrifi  38268  rngolz  38433  rngorz  38434  keridl  38543  lfl0f  39705  lkrlss  39731  lkrscss  39734  lkrin  39800  dihpN  41972  djh02  42049  lclkrlem1  42142  lclkr  42169  mon1psubm  43788  minregex  44122  clsneiel1  44696  stoweidlem22  46594  stoweidlem34  46606  sqwvfoura  46800  elaa2lem  46805  nzrneg1ne0  48850  onsetreclem2  50335