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  910  nfimd  1897  nfald  2321  cbv2w  2333  cbv2  2401  cbv2h  2404  exdistrf  2445  mo4  2559  euind  3685  reuind  3714  sbcimdv  3816  sbcimdvOLD  3817  cores  6206  tz7.7  6348  oprabidw  7393  tz7.49  8396  omsmolem  8608  phpOLD  9173  hta  9842  carddom2  9922  infdif  10154  isf32lem3  10300  alephval2  10517  cfpwsdom  10529  nqerf  10875  zeo  12598  o1rlimmul  15513  catideu  17569  catpropd  17603  ufileu  23307  iscau2  24678  scvxcvx  26372  issgon  32811  cvmsss2  33955  satffunlem2lem1  34085  onsucconni  34985  onsucsuccmpi  34991  bj-peircestab  35092  bj-cbvalimt  35179  bj-cbveximt  35180  bj-ax12v3ALT  35227  bj-wnf2  35259  bj-cbv2hv  35338  bj-sbsb  35378  bj-nfald  35681  lpolsatN  40024  lpolpolsatN  40025  naddcnffo  41757  frege70  42327  sspwtrALT  43226  snlindsntor  46672  0setrec  47269