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

Theorem syl133anc 1205
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 )
syl133anc.8  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  ( et  /\  ze  /\  si ) )  ->  rh )
Assertion
Ref Expression
syl133anc  |-  ( ph  ->  rh )

Proof of Theorem syl133anc
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 . . 3  |-  ( ph  ->  et )
6 sylXanc.6 . . 3  |-  ( ph  ->  ze )
7 sylXanc.7 . . 3  |-  ( ph  ->  si )
85, 6, 73jca 1132 . 2  |-  ( ph  ->  ( et  /\  ze  /\  si ) )
9 syl133anc.8 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  ( et  /\  ze  /\  si ) )  ->  rh )
101, 2, 3, 4, 8, 9syl131anc 1195 1  |-  ( ph  ->  rh )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syl233anc  1211  cgrtr4d  24994  cgrtrand  25002  cgrtr3and  25004  cgrcoml  25005  cgrextendand  25018  segconeu  25020  btwnouttr2  25031  cgr3tr4  25061  cgrxfr  25064  btwnxfr  25065  lineext  25085  brofs2  25086  brifs2  25087  fscgr  25089  btwnconn1lem2  25097  btwnconn1lem4  25099  btwnconn1lem8  25103  btwnconn1lem11  25106  brsegle2  25118  seglecgr12im  25119  segletr  25123  outsidele  25141  dalem13  29683  2llnma1b  29793  cdlemblem  29800  cdlemb  29801  lhpexle3  30019  lhpat  30050  4atex2-0bOLDN  30086  cdlemd4  30208  cdleme14  30280  cdleme19b  30311  cdleme20f  30321  cdleme20j  30325  cdleme20k  30326  cdleme20l2  30328  cdleme20  30331  cdleme22a  30347  cdleme22e  30351  cdleme26e  30366  cdleme28  30380  cdleme38n  30471  cdleme41sn4aw  30482  cdleme41snaw  30483  cdlemg6c  30627  cdlemg6  30630  cdlemg8c  30636  cdlemg9  30641  cdlemg10a  30647  cdlemg12c  30652  cdlemg12d  30653  cdlemg18d  30688  cdlemg18  30689  cdlemg20  30692  cdlemg21  30693  cdlemg22  30694  cdlemg28a  30700  cdlemg33b0  30708  cdlemg28b  30710  cdlemg33a  30713  cdlemg33  30718  cdlemg34  30719  cdlemg36  30721  cdlemg38  30722  cdlemg46  30742  cdlemk6  30844  cdlemki  30848  cdlemksv2  30854  cdlemk11  30856  cdlemk6u  30869  cdleml4N  30986  cdlemn11pre  31218
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