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

Theorem syl322anc 1210
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-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 )
sylXanc.7  |-  ( ph  ->  si )
syl322anc.8  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et )  /\  ( ze  /\  si )
)  ->  rh )
Assertion
Ref Expression
syl322anc  |-  ( ph  ->  rh )

Proof of Theorem syl322anc
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 . 2  |-  ( ph  ->  et )
6 sylXanc.6 . . 3  |-  ( ph  ->  ze )
7 sylXanc.7 . . 3  |-  ( ph  ->  si )
86, 7jca 518 . 2  |-  ( ph  ->  ( ze  /\  si ) )
9 syl322anc.8 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et )  /\  ( ze  /\  si )
)  ->  rh )
101, 2, 3, 4, 5, 8, 9syl321anc 1204 1  |-  ( ph  ->  rh )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ax5seglem6  24634  ax5seg  24638  congsub  27160  mzpcong  27162  jm2.18  27184  jm2.15nn0  27199  jm2.27c  27203  elpaddatriN  30614  paddasslem8  30638  paddasslem12  30642  paddasslem13  30643  pmodlem1  30657  osumcllem5N  30771  pexmidlem2N  30782  cdleme3h  31046  cdleme7ga  31059  cdleme20l  31133  cdleme21ct  31140  cdleme21d  31141  cdleme21e  31142  cdleme26e  31170  cdleme26eALTN  31172  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme39n  31277  cdlemh2  31627  cdlemh  31628  cdlemk12  31661  cdlemk12u  31683  cdlemkfid1N  31732
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