Theorem syl2anc2 585

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  ssnnfiOLD  9169  php4  9212  djulepw  10186  infdjuabs  10200  xrsupss  13287  xrinfmss  13288  trclfv  14946  isumsplit  15785  ram0  16954  0mhm  18699  grpidssd  18898  gexdvds  19451  lsmdisj2  19549  mulgnn0di  19692  odadd1  19715  gsumval3  19774  telgsums  19860  dprdfadd  19889  ringlz  20106  ringrz  20107  lspsneq  20734  dsmmacl  21295  mplsubglem  21557  scmatmhm  22035  mdetuni0  22122  mndifsplit  22137  chfacfscmulgsum  22361  chfacfpmmulgsum  22365  alexsublem  23547  ovolunlem1  25013  mbfi1fseqlem4  25235  deg1lt  25614  deg1invg  25623  sspz  29983  0lno  30038  pjhth  30641  pjhtheu  30642  pjpreeq  30646  opsqrlem1  31388  pfx1s2  32100  orng0le1  32425  0nellinds  32478  qqh1  32960  dnibndlem5  35353  relowlssretop  36239  mettrifi  36620  rngolz  36785  rngorz  36786  keridl  36895  lfl0f  37934  lkrlss  37960  lkrscss  37963  lkrin  38029  dihpN  40202  djh02  40279  lclkrlem1  40372  lclkr  40399  mon1pid  41937  mon1psubm  41938  minregex  42275  clsneiel1  42849  stoweidlem22  44728  stoweidlem34  44740  sqwvfoura  44934  elaa2lem  44939  nzrneg1ne0  46633  rnglz  46654  rngrz  46655  zrrnghm  46706  rnglidl0  46742  rngqiprngimf1  46775  rngqiprngfulem5  46790  onsetreclem2  47741