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

Theorem syli 37
Description: Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004.)
Hypotheses
Ref Expression
syli.1
syli.2
Assertion
Ref Expression
syli

Proof of Theorem syli
StepHypRef Expression
1 syli.1 . 2
2 syli.2 . . 3
32com12 31 . 2
41, 3sylcom 29 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  ibd  243  bija  355  equvini  2087  equveli  2088  equveliOLD  2089  2eu6  2383  rgen2a  2884  rexraleqim  3225  elreldm  5232  tz6.12c  5890  onminex  6642  rntpos  6987  smores  7042  seqomlem2  7135  f1domg  7555  php  7721  fodomnum  8459  carduniima  8498  cardmin  8960  negn0  11197  sqrmo  13085  grpomndo  25348  elghomlem2OLD  25364  isch3  26159  cgrtriv  29652  wl-lem-moexsb  30017
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator