MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl56 Unicode version

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
StepHypRef Expression
1 syl56.1 . 2
2 syl56.2 . . 3
3 syl56.3 . . 3
42, 3syl6 33 . 2
51, 4syl5 32 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator