Theorem syl56 35

Description: Combine syl5 33 and syl6 34. (Contributed by NM, 14-Nov-2013.)

Hypotheses

Ref	Expression
syl56.1	⊢ (𝜑 → 𝜓)
syl56.2	⊢ (𝜒 → (𝜓 → 𝜃))
syl56.3	⊢ (𝜃 → 𝜏)

Assertion

Ref	Expression
syl56	⊢ (𝜒 → (𝜑 → 𝜏))

Proof of Theorem syl56

Step	Hyp	Ref	Expression
1		syl56.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl56.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3		syl56.3	. . 3 ⊢ (𝜃 → 𝜏)
4	2, 3	syl6 34	. 2 ⊢ (𝜒 → (𝜓 → 𝜏))
5	1, 4	syl5 33	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:  spfwOLD  1953  nfald  2151  cbv2h  2257  exdistrf  2321  euind  3360  reuind  3378  sbcimdv  3465  sbcimdvOLD  3466  cores  5555  tz7.7  5666  tz7.49  7427  omsmolem  7620  php  8029  hta  8643  carddom2  8686  infdif  8914  isf32lem3  9060  alephval2  9273  cfpwsdom  9285  nqerf  9631  zeo  11339  o1rlimmul  14197  catideu  16159  catpropd  16192  ufileu  21533  iscau2  22883  scvxcvx  24512  issgon  29513  cvmsss2  30510  onsucconi  31606  onsucsuccmpi  31612  bj-ssbft  31831  bj-ax12v3ALT  31863  bj-cbv2hv  31918  bj-sbsb  32012  wl-dveeq12  32490  lpolsatN  35795  lpolpolsatN  35796  frege70  37247  sspwtrALT  38071  snlindsntor  42054  0setrec  42246