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  909  nfimd  1895  sbi1vOLD  2317  nfald  2336  cbv2w  2346  cbv2  2412  cbv2h  2415  exdistrf  2458  mo4  2584  vtoclgft  3470  euind  3638  reuind  3667  sbcimdv  3766  cores  6079  tz7.7  6195  oprabidw  7181  tz7.49  8091  omsmolem  8290  php  8723  hta  9359  carddom2  9439  infdif  9669  isf32lem3  9815  alephval2  10032  cfpwsdom  10044  nqerf  10390  zeo  12107  o1rlimmul  15023  catideu  17004  catpropd  17037  ufileu  22619  iscau2  23977  scvxcvx  25670  issgon  31610  cvmsss2  32752  satffunlem2lem1  32882  onsucconni  34175  onsucsuccmpi  34181  bj-peircestab  34282  bj-cbvalimt  34366  bj-cbveximt  34367  bj-ax12v3ALT  34414  bj-wnf2  34446  bj-cbv2hv  34515  bj-sbsb  34556  bj-nfald  34832  lpolsatN  39064  lpolpolsatN  39065  frege70  41007  sspwtrALT  41901  snlindsntor  45245  0setrec  45624