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

Theorem syl212anc 1238
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1
sylXanc.2
sylXanc.3
sylXanc.4
sylXanc.5
syl212anc.6
Assertion
Ref Expression
syl212anc

Proof of Theorem syl212anc
StepHypRef Expression
1 sylXanc.1 . 2
2 sylXanc.2 . 2
3 sylXanc.3 . 2
4 sylXanc.4 . . 3
5 sylXanc.5 . . 3
64, 5jca 532 . 2
7 syl212anc.6 . 2
81, 2, 3, 6, 7syl211anc 1234 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  rmob  3430  pntrmax  23749  tglineineq  24023  tglineinteq  24025  paddasslem4  35547  4atexlemu  35788  4atexlemv  35789  cdleme20aN  36035  cdleme20g  36041  cdlemg9a  36358  cdlemg12a  36369  cdlemg17dALTN  36390  cdlemg18b  36405  cdlemg18c  36406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator