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

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

Proof of Theorem syl321anc
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 sylXanc.6 . 2
8 syl321anc.7 . 2
91, 2, 3, 6, 7, 8syl311anc 1242 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  syl322anc  1256  cxple2ad  23106  chordthmlem3  23165  lincext3  33057  4noncolr2  35178  4noncolr1  35179  3atlem5  35211  2lplnj  35344  llnmod2i2  35587  dalawlem11  35605  dalawlem12  35606  cdleme43dN  36218  cdleme4gfv  36233  cdlemeg46nlpq  36243  cdlemg17bq  36399  cdlemg31b0N  36420  cdlemg31b0a  36421  cdlemg31c  36425  cdlemg39  36442  cdlemk47  36675
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