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

Theorem syl322anc 1320
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1  |-  ( ph  ->  ps )
syl12anc.2  |-  ( ph  ->  ch )
syl12anc.3  |-  ( ph  ->  th )
syl22anc.4  |-  ( ph  ->  ta )
syl23anc.5  |-  ( ph  ->  et )
syl33anc.6  |-  ( ph  ->  ze )
syl133anc.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 syl12anc.1 . 2  |-  ( ph  ->  ps )
2 syl12anc.2 . 2  |-  ( ph  ->  ch )
3 syl12anc.3 . 2  |-  ( ph  ->  th )
4 syl22anc.4 . 2  |-  ( ph  ->  ta )
5 syl23anc.5 . 2  |-  ( ph  ->  et )
6 syl33anc.6 . . 3  |-  ( ph  ->  ze )
7 syl133anc.7 . . 3  |-  ( ph  ->  si )
86, 7jca 541 . 2  |-  ( ph  ->  ( ze  /\  si ) )
9 syl322anc.8 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et )  /\  ( ze  /\  si )
)  ->  rh )
101, 2, 3, 4, 5, 8, 9syl321anc 1314 1  |-  ( ph  ->  rh )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  ax5seglem6  25043  ax5seg  25047  elpaddatriN  33439  paddasslem8  33463  paddasslem12  33467  paddasslem13  33468  pmodlem1  33482  osumcllem5N  33596  pexmidlem2N  33607  cdleme3h  33872  cdleme7ga  33885  cdleme20l  33960  cdleme21ct  33967  cdleme21d  33968  cdleme21e  33969  cdleme26e  33997  cdleme26eALTN  33999  cdleme26fALTN  34000  cdleme26f  34001  cdleme26f2ALTN  34002  cdleme26f2  34003  cdleme39n  34104  cdlemh2  34454  cdlemh  34455  cdlemk12  34488  cdlemk12u  34510  cdlemkfid1N  34559  congsub  35891  mzpcong  35893  jm2.18  35914  jm2.15nn0  35929  jm2.27c  35933
  Copyright terms: Public domain W3C validator