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  1895  nfald  2329  cbv2w  2337  cbv2  2403  cbv2h  2406  exdistrf  2447  mo4  2561  euind  3678  reuind  3707  sbcimdv  3805  cores  6191  tz7.7  6327  oprabidw  7372  tz7.49  8359  omsmolem  8567  hta  9785  carddom2  9865  infdif  10094  isf32lem3  10241  alephval2  10458  cfpwsdom  10470  nqerf  10816  zeo  12554  o1rlimmul  15521  catideu  17576  catpropd  17610  ufileu  23829  iscau2  25199  scvxcvx  26918  issgon  34128  cbvex1v  35078  cvmsss2  35310  satffunlem2lem1  35440  onsucconni  36471  onsucsuccmpi  36477  bj-peircestab  36587  bj-cbvalimt  36673  bj-cbveximt  36674  bj-ax12v3ALT  36720  bj-wnf2  36752  bj-cbv2hv  36831  bj-sbsb  36871  bj-nfald  37171  lpolsatN  41527  lpolpolsatN  41528  naddcnffo  43397  frege70  43966  sspwtrALT  44854  snlindsntor  48503  0setrec  49736