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  8485  nnaordi  8557  fineqvlem  9164  dif1ennnALT  9179  xpfiOLD  9220  rankr1ag  9696  cfslb2n  10162  fin23lem27  10222  gchpwdom  10564  prlem934  10927  axpre-sup  11063  cju  12107  xrub  13185  facavg  14155  mulcn2  15438  o1rlimmul  15461  coprm  16547  rpexp  16558  vdwnnlem3  16829  gexdvds  19325  cnpnei  22567  comppfsc  22835  alexsubALTlem3  23352  alexsubALTlem4  23353  iccntr  24136  cfil3i  24585  bcth3  24647  lgseisenlem2  26676  cusgredg  28201  uspgr2wlkeq  28423  ubthlem1  29641  staddi  31017  stadd3i  31019  addltmulALT  31217  cnre2csqlem  32303  tpr2rico  32305  satffunlem2lem1  33810  mclsax  33975  dfrdg4  34474  segconeq  34533  nn0prpwlem  34732  bj-bary1lem1  35720  poimirlem29  36045  fdc  36142  bfplem2  36220  atexchcvrN  37841  dalem3  38065  cdleme3h  38636  cdleme21ct  38730  oexpreposd  40716  cantnfresb  41565  omabs2  41572  sbgoldbwt  45870  sbgoldbst  45871  nnsum4primesodd  45889  nnsum4primesoddALTV  45890  dignn0flhalflem1  46602
  Copyright terms: Public domain W3C validator