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  922  nfimd  1913  nfald  2359  cbv2w  2367  cbv2  2433  cbv2h  2436  exdistrf  2477  mo4  2592  euind  3685  reuind  3714  sbcimdv  3810  cores  6231  tz7.7  6367  oprabidw  7422  tz7.49  8410  omsmolem  8621  hta  9849  carddom2  9929  infdif  10158  isf32lem3  10306  alephval2  10524  cfpwsdom  10536  nqerf  10882  zeo  12653  o1rlimmul  15637  catideu  17698  catpropd  17732  ufileu  23967  iscau2  25327  scvxcvx  27038  issgon  34381  cbvex1v  35330  cvmsss2  35585  satffunlem2lem1  35715  onsucconni  36758  onsucsuccmpi  36764  dfttc4lem2  36850  regsfromunir1  36861  bj-peircestab  36954  bj-ax12v3ALT  37122  bj-wnf2  37156  bj-cbv2hv  37243  bj-sbsb  37283  bj-nfald  37588  lpolsatN  42073  lpolpolsatN  42074  naddcnffo  43902  frege70  44470  sspwtrALT  45358  snlindsntor  49054  0setrec  50286