Theorem syl56 36

Description: Combine syl5 34 and syl6 35. (Contributed by NM, 14-Nov-2013.)

Hypotheses

Ref	Expression
syl56.1	|- ( ph -> ps )
syl56.2	|- ( ch -> ( ps -> th ) )
syl56.3	|- ( th -> ta )

Assertion

Ref	Expression
syl56	|- ( ch -> ( ph -> ta ) )

Proof of Theorem syl56

Step	Hyp	Ref	Expression
1		syl56.1	. 2 |- ( ph -> ps )
2		syl56.2	. . 3 |- ( ch -> ( ps -> th ) )
3		syl56.3	. . 3 |- ( th -> ta )
4	2, 3	syl6 35	. 2 |- ( ch -> ( ps -> ta ) )
5	1, 4	syl5 34	1 |- ( ch -> ( ph -> ta ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  spfwOLD  1966  nfald  2165  cbv2h  2269  exdistrf  2333  euind  3393  reuind  3411  sbcimdv  3498  sbcimdvOLD  3499  cores  5638  tz7.7  5749  tz7.49  7540  omsmolem  7733  php  8144  hta  8760  carddom2  8803  infdif  9031  isf32lem3  9177  alephval2  9394  cfpwsdom  9406  nqerf  9752  zeo  11463  o1rlimmul  14349  catideu  16336  catpropd  16369  ufileu  21723  iscau2  23075  scvxcvx  24712  issgon  30186  cvmsss2  31256  onsucconni  32436  onsucsuccmpi  32442  bj-ssbft  32642  bj-ax12v3ALT  32676  bj-cbv2hv  32731  bj-sbsb  32824  wl-dveeq12  33311  lpolsatN  36777  lpolpolsatN  36778  frege70  38227  sspwtrALT  39049  snlindsntor  42260  0setrec  42447