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 ⊢ (𝜒 → (𝜑 → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  orim12dALT  925  nfimd  1927  nfald  2363  cbv2w  2371  cbv2  2437  cbv2h  2440  exdistrf  2481  mo4  2596  euind  3689  reuind  3718  sbcimdv  3814  cores  6252  tz7.7  6390  oprabidw  7447  tz7.49  8434  omsmolem  8645  hta  9894  htaOLD  9895  carddom2  9975  infdif  10203  isf32lem3  10350  alephval2  10568  cfpwsdom  10580  nqerf  10926  zeo  12693  o1rlimmul  15689  catideu  17748  catpropd  17782  ufileu  24105  iscau2  25465  scvxcvx  27179  issgon  34536  cbvex1v  35486  cvmsss2  35779  satffunlem2lem1  35909  onsucconni  36981  onsucsuccmpi  36987  dfttc4lem2  37073  regsfromunir1  37084  bj-peircestab  37176  bj-ax12v3ALT  37344  bj-wnf2  37378  bj-cbv2hv  37465  bj-sbsb  37505  bj-nfald  37812  lpolsatN  42295  lpolpolsatN  42296  naddcnffo  44124  frege70  44692  sspwtrALT  45563  snlindsntor  49284  0setrec  50515