Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2anc2 Structured version   Visualization version   GIF version

Theorem syl2anc2 589
 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
StepHypRef Expression
1 syl2anc2.1 . 2 (𝜑𝜓)
2 syl2anc2.2 . . 3 (𝜓𝜒)
31, 2syl 17 . 2 (𝜑𝜒)
4 syl2anc2.3 . 2 ((𝜓𝜒) → 𝜃)
51, 3, 4syl2anc 588 1 (𝜑𝜃)
 Colors of variables: wff setvar class 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  8726  ssnnfi  8759  djulepw  9645  infdjuabs  9659  xrsupss  12736  xrinfmss  12737  trclfv  14400  isumsplit  15236  ram0  16406  0mhm  18043  grpidssd  18235  gexdvds  18769  lsmdisj2  18868  mulgnn0di  19007  odadd1  19029  gsumval3  19088  telgsums  19174  dprdfadd  19203  ringlz  19401  ringrz  19402  lspsneq  19955  dsmmacl  20499  mplsubglem  20757  scmatmhm  21227  mdetuni0  21314  mndifsplit  21329  chfacfscmulgsum  21553  chfacfpmmulgsum  21557  alexsublem  22737  ovolunlem1  24190  mbfi1fseqlem4  24411  deg1lt  24790  deg1invg  24799  sspz  28610  0lno  28665  pjhth  29268  pjhtheu  29269  pjpreeq  29273  opsqrlem1  30015  pfx1s2  30730  orng0le1  31030  0nellinds  31080  qqh1  31447  dnibndlem5  34204  relowlssretop  35053  mettrifi  35468  rngolz  35633  rngorz  35634  keridl  35743  lfl0f  36638  lkrlss  36664  lkrscss  36667  lkrin  36733  dihpN  38905  djh02  38982  lclkrlem1  39075  lclkr  39102  mon1pid  40515  mon1psubm  40516  clsneiel1  41177  stoweidlem22  43023  stoweidlem34  43035  sqwvfoura  43229  elaa2lem  43234  nzrneg1ne0  44853  rnglz  44868  zrrnghm  44901  onsetreclem2  45619
 Copyright terms: Public domain W3C validator