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

Theorem syl322anc 1247
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 532 . 2  |-  ( ph  ->  ( ze  /\  si ) )
9 syl322anc.8 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et )  /\  ( ze  /\  si )
)  ->  rh )
101, 2, 3, 4, 5, 8, 9syl321anc 1241 1  |-  ( ph  ->  rh )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  ax5seglem6  23352  ax5seg  23356  congsub  29481  mzpcong  29483  jm2.18  29505  jm2.15nn0  29520  jm2.27c  29524  elpaddatriN  33805  paddasslem8  33829  paddasslem12  33833  paddasslem13  33834  pmodlem1  33848  osumcllem5N  33962  pexmidlem2N  33973  cdleme3h  34237  cdleme7ga  34250  cdleme20l  34324  cdleme21ct  34331  cdleme21d  34332  cdleme21e  34333  cdleme26e  34361  cdleme26eALTN  34363  cdleme26fALTN  34364  cdleme26f  34365  cdleme26f2ALTN  34366  cdleme26f2  34367  cdleme39n  34468  cdlemh2  34818  cdlemh  34819  cdlemk12  34852  cdlemk12u  34874  cdlemkfid1N  34923
  Copyright terms: Public domain W3C validator