Theorem syl56 37

Description: Combine syl5 35 and syl6 36. (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 36	. 2 ⊢ (𝜒 → (𝜓 → 𝜏))
5	1, 4	syl5 35	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  924  nfimd  1921  nfald  2367  cbv2w  2375  cbv2  2441  cbv2h  2444  exdistrf  2485  mo4  2600  euind  3696  reuind  3725  sbcimdv  3821  cores  6247  tz7.7  6383  oprabidw  7439  tz7.49  8428  omsmolem  8639  hta  9879  carddom2  9959  infdif  10187  isf32lem3  10335  alephval2  10553  cfpwsdom  10565  nqerf  10911  zeo  12678  o1rlimmul  15666  catideu  17727  catpropd  17761  ufileu  24041  iscau2  25401  scvxcvx  27112  issgon  34454  cbvex1v  35403  cvmsss2  35661  satffunlem2lem1  35791  onsucconni  36833  onsucsuccmpi  36839  dfttc4lem2  36925  regsfromunir1  36936  bj-peircestab  37028  bj-ax12v3ALT  37196  bj-wnf2  37230  bj-cbv2hv  37317  bj-sbsb  37357  bj-nfald  37662  lpolsatN  42147  lpolpolsatN  42148  naddcnffo  43976  frege70  44544  sspwtrALT  45415  snlindsntor  49129  0setrec  50360