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  3695  reuind  3724  sbcimdv  3822  cores  6222  tz7.7  6358  oprabidw  7418  tz7.49  8413  omsmolem  8621  hta  9850  carddom2  9930  infdif  10161  isf32lem3  10308  alephval2  10525  cfpwsdom  10537  nqerf  10883  zeo  12620  o1rlimmul  15585  catideu  17636  catpropd  17670  ufileu  23806  iscau2  25177  scvxcvx  26896  issgon  34113  cbvex1v  35064  cvmsss2  35261  satffunlem2lem1  35391  onsucconni  36425  onsucsuccmpi  36431  bj-peircestab  36541  bj-cbvalimt  36627  bj-cbveximt  36628  bj-ax12v3ALT  36674  bj-wnf2  36706  bj-cbv2hv  36785  bj-sbsb  36825  bj-nfald  37125  lpolsatN  41482  lpolpolsatN  41483  naddcnffo  43353  frege70  43922  sspwtrALT  44811  snlindsntor  48460  0setrec  49693