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

Theorem syl9 71
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
Hypotheses
Ref Expression
syl9.1
syl9.2
Assertion
Ref Expression
syl9

Proof of Theorem syl9
StepHypRef Expression
1 syl9.1 . 2
2 syl9.2 . . 3
32a1i 11 . 2
41, 3syl5d 67 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  syl9r  72  com23  78  sylan9  657  19.21t  1904  axc9lem1  2001  axc9lem2  2040  axc11n  2049  axc11nOLD  2050  sbequi  2116  reuss2  3777  reupick  3781  ordtr2  4927  suc11  4986  elres  5314  funimass4  5924  fliftfun  6210  omlimcl  7246  nneob  7320  rankwflemb  8232  cflm  8651  domtriomlem  8843  grothomex  9228  sup3  10525  caubnd  13191  fbflim2  20478  ellimc3  22283  3cyclfrgrarn1  25012  dfon2lem6  29220  opnrebl2  30139  pm11.71  31303  axc11next  31313  bj-axc11nv  34316  stdpc5t  34400  diaintclN  36785  dibintclN  36894  dihintcl  37071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator