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

Theorem syl331anc 1210
 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 1135 . 2
8 sylXanc.7 . 2
9 syl331anc.8 . 2
101, 2, 3, 7, 8, 9syl311anc 1199 1
 Colors of variables: wff set class Syntax hints:   wi 4   w3a 937 This theorem is referenced by:  syl332anc  1216  syl333anc  1217  qredeu  13109  brbtwn2  25846  3atlem4  30345  3atlem6  30347  llnexchb2  30728  osumcllem9N  30823  cdlemd4  31060  cdleme26fALTN  31221  cdleme26f  31222  cdleme36m  31320  cdlemg17b  31521  cdlemg17h  31527  cdlemk38  31774  cdlemk53b  31815  cdlemkyyN  31821  cdlemk43N  31822 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
 Copyright terms: Public domain W3C validator