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  917  nfimd  1901  nfald  2337  cbv2w  2345  cbv2  2411  cbv2h  2414  exdistrf  2455  mo4  2570  euind  3672  reuind  3701  sbcimdv  3798  cores  6207  tz7.7  6343  oprabidw  7394  tz7.49  8381  omsmolem  8590  hta  9819  carddom2  9899  infdif  10128  isf32lem3  10275  alephval2  10493  cfpwsdom  10505  nqerf  10851  zeo  12613  o1rlimmul  15579  catideu  17639  catpropd  17673  ufileu  23909  iscau2  25269  scvxcvx  26974  issgon  34314  cbvex1v  35263  cvmsss2  35509  satffunlem2lem1  35639  onsucconni  36672  onsucsuccmpi  36678  dfttc4lem2  36764  regsfromunir1  36775  bj-peircestab  36868  bj-ax12v3ALT  37036  bj-wnf2  37070  bj-cbv2hv  37157  bj-sbsb  37197  bj-nfald  37502  lpolsatN  41987  lpolpolsatN  41988  naddcnffo  43816  frege70  44384  sspwtrALT  45272  snlindsntor  48969  0setrec  50201