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

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

Proof of Theorem syl331anc
StepHypRef Expression
1 sylXanc.1 . 2
2 sylXanc.2 . 2
3 sylXanc.3 . 2
4 sylXanc.4 . . 3
5 sylXanc.5 . . 3
6 sylXanc.6 . . 3
74, 5, 63jca 1176 . 2
8 sylXanc.7 . 2
9 syl331anc.8 . 2
101, 2, 3, 7, 8, 9syl311anc 1242 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  syl332anc  1259  syl333anc  1260  qredeu  14248  brbtwn2  24208  3atlem4  35210  3atlem6  35212  llnexchb2  35593  osumcllem9N  35688  cdlemd4  35926  cdleme26fALTN  36088  cdleme26f  36089  cdleme36m  36187  cdlemg17b  36388  cdlemg17h  36394  cdlemk38  36641  cdlemk53b  36682  cdlemkyyN  36688  cdlemk43N  36689
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