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  24562  ax5seg  24566  congsub  27057  mzpcong  27059  jm2.18  27081  jm2.15nn0  27096  jm2.27c  27100  elpaddatriN  29992  paddasslem8  30016  paddasslem12  30020  paddasslem13  30021  pmodlem1  30035  osumcllem5N  30149  pexmidlem2N  30160  cdleme3h  30424  cdleme7ga  30437  cdleme20l  30511  cdleme21ct  30518  cdleme21d  30519  cdleme21e  30520  cdleme26e  30548  cdleme26eALTN  30550  cdleme26fALTN  30551  cdleme26f  30552  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme39n  30655  cdlemh2  31005  cdlemh  31006  cdlemk12  31039  cdlemk12u  31061  cdlemkfid1N  31110
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