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

Theorem syl231anc 1284
 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
syl231anc.7
Assertion
Ref Expression
syl231anc

Proof of Theorem syl231anc
StepHypRef Expression
1 sylXanc.1 . . 3
2 sylXanc.2 . . 3
31, 2jca 534 . 2
4 sylXanc.3 . 2
5 sylXanc.4 . 2
6 sylXanc.5 . 2
7 sylXanc.6 . 2
8 syl231anc.7 . 2
93, 4, 5, 6, 7, 8syl131anc 1277 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3a 982 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 188  df-an 372  df-3an 984 This theorem is referenced by:  syl232anc  1291  isosctr  23641  axeuclid  24865  dalawlem3  33176  dalawlem6  33179  cdlemd7  33508  cdleme18c  33597  cdlemi  34125  cdlemk7  34153  cdlemk11  34154  cdlemk7u  34175  cdlemk11u  34176  cdlemk19xlem  34247  cdlemk55u1  34270  cdlemk56  34276
 Copyright terms: Public domain W3C validator