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

Theorem syl312anc 1203
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 518 . 2  |-  ( ph  ->  ( et  /\  ze ) )
8 syl312anc.7 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta  /\  ( et  /\  ze ) )  ->  si )
91, 2, 3, 4, 7, 8syl311anc 1196 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  pythagtriplem19  12886  cdleme27cl  30555  cdlemefs27cl  30602  cdleme32fvcl  30629  cdlemg16ALTN  30847  cdlemg27a  30881  cdlemg31c  30888  cdlemg39  30905  cdlemk11ta  31118  cdlemk19ylem  31119  cdlemk11tc  31134  cdlemk45  31136  dihmeetlem12N  31508  dihjatc  31607
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator