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

Theorem syl321anc 1286
Description: Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
sylXanc.5  |-  ( ph  ->  et )
sylXanc.6  |-  ( ph  ->  ze )
syl321anc.7  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et )  /\  ze )  ->  si )
Assertion
Ref Expression
syl321anc  |-  ( ph  ->  si )

Proof of Theorem syl321anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . 2  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
5 sylXanc.5 . . 3  |-  ( ph  ->  et )
64, 5jca 534 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 sylXanc.6 . 2  |-  ( ph  ->  ze )
8 syl321anc.7 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et )  /\  ze )  ->  si )
91, 2, 3, 6, 7, 8syl311anc 1278 1  |-  ( ph  ->  si )
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:  syl322anc  1292  cxple2ad  23535  chordthmlem3  23625  4noncolr2  32728  4noncolr1  32729  3atlem5  32761  2lplnj  32894  llnmod2i2  33137  dalawlem11  33155  dalawlem12  33156  cdleme43dN  33768  cdleme4gfv  33783  cdlemeg46nlpq  33793  cdlemg17bq  33949  cdlemg31b0N  33970  cdlemg31b0a  33971  cdlemg31c  33975  cdlemg39  33992  cdlemk47  34225  lincext3  39009
  Copyright terms: Public domain W3C validator