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

Theorem syl312anc 1205
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 519 . 2  |-  ( ph  ->  ( et  /\  ze ) )
8 syl312anc.7 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta  /\  ( et  /\  ze ) )  ->  si )
91, 2, 3, 4, 7, 8syl311anc 1198 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  pythagtriplem19  13170  cdleme27cl  30860  cdlemefs27cl  30907  cdleme32fvcl  30934  cdlemg16ALTN  31152  cdlemg27a  31186  cdlemg31c  31193  cdlemg39  31210  cdlemk11ta  31423  cdlemk19ylem  31424  cdlemk11tc  31439  cdlemk45  31441  dihmeetlem12N  31813  dihjatc  31912
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator