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

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
StepHypRef Expression
1 syl2anc2.1 . 2 (𝜑𝜓)
2 syl2anc2.2 . . 3 (𝜓𝜒)
31, 2syl 17 . 2 (𝜑𝜒)
4 syl2anc2.3 . 2 ((𝜓𝜒) → 𝜃)
51, 3, 4syl2anc 584 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  php4  9250  djulepw  10233  infdjuabs  10245  xrsupss  13351  xrinfmss  13352  trclfv  15039  isumsplit  15876  ram0  17060  0mhm  18832  grpidssd  19034  gexdvds  19602  lsmdisj2  19700  mulgnn0di  19843  odadd1  19866  gsumval3  19925  telgsums  20011  dprdfadd  20040  rnglz  20162  rngrz  20163  zrrnghm  20536  lspsneq  21124  rnglidl0  21239  rngqiprngimf1  21310  rngqiprngfulem5  21325  dsmmacl  21761  mplsubglem  22019  scmatmhm  22540  mdetuni0  22627  mndifsplit  22642  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  alexsublem  24052  ovolunlem1  25532  mbfi1fseqlem4  25753  deg1lt  26136  deg1invg  26145  mon1pid  26193  sspz  30754  0lno  30809  pjhth  31412  pjhtheu  31413  pjpreeq  31417  opsqrlem1  32159  pfx1s2  32923  gsumwun  33068  orng0le1  33342  0nellinds  33398  irredminply  33757  qqh1  33986  dnibndlem5  36483  relowlssretop  37364  mettrifi  37764  rngolz  37929  rngorz  37930  keridl  38039  lfl0f  39070  lkrlss  39096  lkrscss  39099  lkrin  39165  dihpN  41338  djh02  41415  lclkrlem1  41508  lclkr  41535  mon1psubm  43211  minregex  43547  clsneiel1  44121  stoweidlem22  46037  stoweidlem34  46049  sqwvfoura  46243  elaa2lem  46248  nzrneg1ne0  48146  onsetreclem2  49225
  Copyright terms: Public domain W3C validator