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

Step	Hyp	Ref	Expression
1		3syld.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		3syld.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜃))
3	1, 2	syld 47	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4		3syld.3	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
5	3, 4	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜏))

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  7586  nnaordi  7658  fineqvlem  8134  dif1en  8153  xpfi  8191  rankr1ag  8625  cfslb2n  9050  fin23lem27  9110  gchpwdom  9452  prlem934  9815  axpre-sup  9950  cju  10976  xrub  12101  facavg  13044  mulcn2  14276  o1rlimmul  14299  coprm  15366  rpexp  15375  vdwnnlem3  15644  gexdvds  17939  cnpnei  21008  comppfsc  21275  alexsubALTlem3  21793  alexsubALTlem4  21794  iccntr  22564  cfil3i  23007  bcth3  23068  lgseisenlem2  25035  cusgredg  26241  uspgr2wlkeq  26445  frgrwopreglem4  27076  ubthlem1  27614  staddi  28993  stadd3i  28995  addltmulALT  29193  cnre2csqlem  29780  tpr2rico  29782  mclsax  31227  dfrdg4  31753  segconeq  31812  nn0prpwlem  32012  bj-bary1lem1  32833  poimirlem29  33109  fdc  33212  bfplem2  33293  atexchcvrN  34245  dalem3  34469  cdleme3h  35041  cdleme21ct  35136  bgoldbwt  40990  bgoldbst  40991  nnsum4primesodd  41003  nnsum4primesoddALTV  41004  dignn0flhalflem1  41731