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  8159  nnaordi  8231  fineqvlem  8720  dif1en  8739  xpfi  8777  rankr1ag  9219  cfslb2n  9683  fin23lem27  9743  gchpwdom  10085  prlem934  10448  axpre-sup  10584  cju  11625  xrub  12697  facavg  13661  mulcn2  14948  o1rlimmul  14971  coprm  16049  rpexp  16058  vdwnnlem3  16327  gexdvds  18705  cnpnei  21873  comppfsc  22141  alexsubALTlem3  22658  alexsubALTlem4  22659  iccntr  23430  cfil3i  23877  bcth3  23939  lgseisenlem2  25964  cusgredg  27218  uspgr2wlkeq  27439  ubthlem1  28657  staddi  30033  stadd3i  30035  addltmulALT  30233  cnre2csqlem  31267  tpr2rico  31269  satffunlem2lem1  32765  mclsax  32930  dfrdg4  33526  segconeq  33585  nn0prpwlem  33784  bj-bary1lem1  34726  poimirlem29  35085  fdc  35182  bfplem2  35260  atexchcvrN  36735  dalem3  36959  cdleme3h  37530  cdleme21ct  37624  oexpreposd  39484  sbgoldbwt  44292  sbgoldbst  44293  nnsum4primesodd  44311  nnsum4primesoddALTV  44312  dignn0flhalflem1  45026
  Copyright terms: Public domain W3C validator