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  2402  cbv2h  2405  exdistrf  2446  mo4  2560  euind  3698  reuind  3727  sbcimdv  3825  cores  6225  tz7.7  6361  oprabidw  7421  tz7.49  8416  omsmolem  8624  hta  9857  carddom2  9937  infdif  10168  isf32lem3  10315  alephval2  10532  cfpwsdom  10544  nqerf  10890  zeo  12627  o1rlimmul  15592  catideu  17643  catpropd  17677  ufileu  23813  iscau2  25184  scvxcvx  26903  issgon  34120  cbvex1v  35071  cvmsss2  35268  satffunlem2lem1  35398  onsucconni  36432  onsucsuccmpi  36438  bj-peircestab  36548  bj-cbvalimt  36634  bj-cbveximt  36635  bj-ax12v3ALT  36681  bj-wnf2  36713  bj-cbv2hv  36792  bj-sbsb  36832  bj-nfald  37132  lpolsatN  41489  lpolpolsatN  41490  naddcnffo  43360  frege70  43929  sspwtrALT  44818  snlindsntor  48464  0setrec  49697