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

Theorem 3syld 58
 Description: Triple syllogism deduction. Deduction associated with 3syld 58. (Contributed by Jeff Hankins, 4-Aug-2009.)
Hypotheses
Ref Expression
3syld.1 (𝜑 → (𝜓𝜒))
3syld.2 (𝜑 → (𝜒𝜃))
3syld.3 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
3syld (𝜑 → (𝜓𝜏))

Proof of Theorem 3syld
StepHypRef Expression
1 3syld.1 . . 3 (𝜑 → (𝜓𝜒))
2 3syld.2 . . 3 (𝜑 → (𝜒𝜃))
31, 2syld 46 . 2 (𝜑 → (𝜓𝜃))
4 3syld.3 . 2 (𝜑 → (𝜃𝜏))
53, 4syld 46 1 (𝜑 → (𝜓𝜏))
 Colors of variables: wff setvar class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7 This theorem is referenced by:  oaordi  7513  nnaordi  7585  fineqvlem  8059  dif1en  8078  xpfi  8116  rankr1ag  8548  cfslb2n  8973  fin23lem27  9033  gchpwdom  9371  prlem934  9734  axpre-sup  9869  cju  10893  xrub  12014  facavg  12950  mulcn2  14174  o1rlimmul  14197  coprm  15261  rpexp  15270  vdwnnlem3  15539  gexdvds  17822  cnpnei  20878  comppfsc  21145  alexsubALTlem3  21663  alexsubALTlem4  21664  iccntr  22432  cfil3i  22875  bcth3  22936  lgseisenlem2  24901  usgrasscusgra  26011  usg2wlkeq  26236  nbhashuvtx1  26442  frgrawopreglem4  26574  ubthlem1  27110  staddi  28489  stadd3i  28491  addltmulALT  28689  cnre2csqlem  29284  tpr2rico  29286  mclsax  30720  dfrdg4  31228  segconeq  31287  nn0prpwlem  31487  bj-bary1lem1  32338  poimirlem29  32608  fdc  32711  bfplem2  32792  atexchcvrN  33744  dalem3  33968  cdleme3h  34540  cdleme21ct  34635  bgoldbwt  40199  bgoldbst  40200  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  cusgredg  40646  uspgr2wlkeq  40854  frgrwopreglem4  41484  dignn0flhalflem1  42207
 Copyright terms: Public domain W3C validator