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

Theorem 3syld 60
Description: Triple syllogism deduction. Deduction associated with 3syld 60. (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 47 . 2 (𝜑 → (𝜓𝜃))
4 3syld.3 . 2 (𝜑 → (𝜃𝜏))
53, 4syld 47 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  7780  nnaordi  7852  fineqvlem  8330  dif1en  8349  xpfi  8387  rankr1ag  8829  cfslb2n  9292  fin23lem27  9352  gchpwdom  9694  prlem934  10057  axpre-sup  10192  cju  11218  xrub  12347  facavg  13292  mulcn2  14534  o1rlimmul  14557  coprm  15630  rpexp  15639  vdwnnlem3  15908  gexdvds  18206  cnpnei  21289  comppfsc  21556  alexsubALTlem3  22073  alexsubALTlem4  22074  iccntr  22844  cfil3i  23286  bcth3  23347  lgseisenlem2  25322  cusgredg  26555  uspgr2wlkeq  26777  ubthlem1  28066  staddi  29445  stadd3i  29447  addltmulALT  29645  cnre2csqlem  30296  tpr2rico  30298  mclsax  31804  dfrdg4  32395  segconeq  32454  nn0prpwlem  32654  bj-bary1lem1  33498  poimirlem29  33771  fdc  33873  bfplem2  33954  atexchcvrN  35248  dalem3  35472  cdleme3h  36044  cdleme21ct  36138  sbgoldbwt  42193  sbgoldbst  42194  nnsum4primesodd  42212  nnsum4primesoddALTV  42213  dignn0flhalflem1  42937
  Copyright terms: Public domain W3C validator