Theorem syl56 36

Description: Combine syl5 34 and syl6 35. (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 35	. 2 ⊢ (𝜒 → (𝜓 → 𝜏))
5	1, 4	syl5 34	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:  orim12dALT  911  nfimd  1894  nfald  2327  cbv2w  2335  cbv2  2401  cbv2h  2404  exdistrf  2445  mo4  2559  euind  3686  reuind  3715  sbcimdv  3813  cores  6202  tz7.7  6337  oprabidw  7384  tz7.49  8374  omsmolem  8582  hta  9812  carddom2  9892  infdif  10121  isf32lem3  10268  alephval2  10485  cfpwsdom  10497  nqerf  10843  zeo  12580  o1rlimmul  15544  catideu  17599  catpropd  17633  ufileu  23822  iscau2  25193  scvxcvx  26912  issgon  34092  cbvex1v  35043  cvmsss2  35249  satffunlem2lem1  35379  onsucconni  36413  onsucsuccmpi  36419  bj-peircestab  36529  bj-cbvalimt  36615  bj-cbveximt  36616  bj-ax12v3ALT  36662  bj-wnf2  36694  bj-cbv2hv  36773  bj-sbsb  36813  bj-nfald  37113  lpolsatN  41470  lpolpolsatN  41471  naddcnffo  43340  frege70  43909  sspwtrALT  44798  snlindsntor  48460  0setrec  49693