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

Theorem syl312anc 1206
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 )
syl312anc.7  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta  /\  ( et  /\  ze ) )  ->  si )
Assertion
Ref Expression
syl312anc  |-  ( ph  ->  si )

Proof of Theorem syl312anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . 2  |-  ( ph  ->  th )
4 sylXanc.4 . 2  |-  ( ph  ->  ta )
5 sylXanc.5 . . 3  |-  ( ph  ->  et )
6 sylXanc.6 . . 3  |-  ( ph  ->  ze )
75, 6jca 520 . 2  |-  ( ph  ->  ( et  /\  ze ) )
8 syl312anc.7 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta  /\  ( et  /\  ze ) )  ->  si )
91, 2, 3, 4, 7, 8syl311anc 1199 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  pythagtriplem19  13212  cdleme27cl  31237  cdlemefs27cl  31284  cdleme32fvcl  31311  cdlemg16ALTN  31529  cdlemg27a  31563  cdlemg31c  31570  cdlemg39  31587  cdlemk11ta  31800  cdlemk19ylem  31801  cdlemk11tc  31816  cdlemk45  31818  dihmeetlem12N  32190  dihjatc  32289
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator