Theorem syl56 34

Description: Combine syl5 32 and syl6 33. (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 33	. 2
5	1, 4	syl5 32	1

Syntax hints:  ->wi 4

This theorem is referenced by:  spfw  1806  19.8aOLD  1858  cbv2h  2019  exdistrf  2075  euind  3286  reuind  3303  sbcimdv  3396  tz7.7  4909  cores  5515  tz7.49  7129  omsmolem  7321  php  7721  hta  8336  carddom2  8379  infdif  8610  isf32lem3  8756  alephval2  8968  cfpwsdom  8980  nqerf  9329  zeo  10973  o1rlimmul  13441  catideu  15072  catpropd  15104  ufileu  20420  iscau2  21716  scvxcvx  23315  issgon  28123  cvmsss2  28719  onsucconi  29902  onsucsuccmpi  29908  snlindsntor  33072  sspwtrALT  33620  bj-cbv2hv  34294  lpolsatN  37215  lpolpolsatN  37216

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