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

Theorem syl322anc 1256
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 530 . 2  |-  ( ph  ->  ( ze  /\  si ) )
9 syl322anc.8 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et )  /\  ( ze  /\  si )
)  ->  rh )
101, 2, 3, 4, 5, 8, 9syl321anc 1250 1  |-  ( ph  ->  rh )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 972
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 369  df-3an 974
This theorem is referenced by:  ax5seglem6  24536  ax5seg  24540  elpaddatriN  32784  paddasslem8  32808  paddasslem12  32812  paddasslem13  32813  pmodlem1  32827  osumcllem5N  32941  pexmidlem2N  32952  cdleme3h  33217  cdleme7ga  33230  cdleme20l  33305  cdleme21ct  33312  cdleme21d  33313  cdleme21e  33314  cdleme26e  33342  cdleme26eALTN  33344  cdleme26fALTN  33345  cdleme26f  33346  cdleme26f2ALTN  33347  cdleme26f2  33348  cdleme39n  33449  cdlemh2  33799  cdlemh  33800  cdlemk12  33833  cdlemk12u  33855  cdlemkfid1N  33904  congsub  35233  mzpcong  35235  jm2.18  35256  jm2.15nn0  35271  jm2.27c  35275
  Copyright terms: Public domain W3C validator