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  7571  nnaordi  7643  fineqvlem  8118  dif1en  8137  xpfi  8175  rankr1ag  8609  cfslb2n  9034  fin23lem27  9094  gchpwdom  9436  prlem934  9799  axpre-sup  9934  cju  10960  xrub  12085  facavg  13028  mulcn2  14260  o1rlimmul  14283  coprm  15347  rpexp  15356  vdwnnlem3  15625  gexdvds  17920  cnpnei  20978  comppfsc  21245  alexsubALTlem3  21763  alexsubALTlem4  21764  iccntr  22532  cfil3i  22975  bcth3  23036  lgseisenlem2  25001  cusgredg  26207  uspgr2wlkeq  26411  frgrwopreglem4  27042  ubthlem1  27572  staddi  28951  stadd3i  28953  addltmulALT  29151  cnre2csqlem  29735  tpr2rico  29737  mclsax  31171  dfrdg4  31697  segconeq  31756  nn0prpwlem  31956  bj-bary1lem1  32791  poimirlem29  33067  fdc  33170  bfplem2  33251  atexchcvrN  34203  dalem3  34427  cdleme3h  34999  cdleme21ct  35094  bgoldbwt  40957  bgoldbst  40958  nnsum4primesodd  40970  nnsum4primesoddALTV  40971  dignn0flhalflem1  41698
  Copyright terms: Public domain W3C validator