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  3692  reuind  3721  sbcimdv  3819  cores  6210  tz7.7  6346  oprabidw  7400  tz7.49  8390  omsmolem  8598  hta  9826  carddom2  9906  infdif  10137  isf32lem3  10284  alephval2  10501  cfpwsdom  10513  nqerf  10859  zeo  12596  o1rlimmul  15561  catideu  17612  catpropd  17646  ufileu  23782  iscau2  25153  scvxcvx  26872  issgon  34086  cbvex1v  35037  cvmsss2  35234  satffunlem2lem1  35364  onsucconni  36398  onsucsuccmpi  36404  bj-peircestab  36514  bj-cbvalimt  36600  bj-cbveximt  36601  bj-ax12v3ALT  36647  bj-wnf2  36679  bj-cbv2hv  36758  bj-sbsb  36798  bj-nfald  37098  lpolsatN  41455  lpolpolsatN  41456  naddcnffo  43326  frege70  43895  sspwtrALT  44784  snlindsntor  48433  0setrec  49666