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  24608  cgrtrand  24616  cgrtr3and  24618  cgrcoml  24619  cgrextendand  24632  segconeu  24634  btwnouttr2  24645  cgr3tr4  24675  cgrxfr  24678  btwnxfr  24679  lineext  24699  brofs2  24700  brifs2  24701  fscgr  24703  btwnconn1lem2  24711  btwnconn1lem4  24713  btwnconn1lem8  24717  btwnconn1lem11  24720  brsegle2  24732  seglecgr12im  24733  segletr  24737  outsidele  24755  dalem13  29865  2llnma1b  29975  cdlemblem  29982  cdlemb  29983  lhpexle3  30201  lhpat  30232  4atex2-0bOLDN  30268  cdlemd4  30390  cdleme14  30462  cdleme19b  30493  cdleme20f  30503  cdleme20j  30507  cdleme20k  30508  cdleme20l2  30510  cdleme20  30513  cdleme22a  30529  cdleme22e  30533  cdleme26e  30548  cdleme28  30562  cdleme38n  30653  cdleme41sn4aw  30664  cdleme41snaw  30665  cdlemg6c  30809  cdlemg6  30812  cdlemg8c  30818  cdlemg9  30823  cdlemg10a  30829  cdlemg12c  30834  cdlemg12d  30835  cdlemg18d  30870  cdlemg18  30871  cdlemg20  30874  cdlemg21  30875  cdlemg22  30876  cdlemg28a  30882  cdlemg33b0  30890  cdlemg28b  30892  cdlemg33a  30895  cdlemg33  30900  cdlemg34  30901  cdlemg36  30903  cdlemg38  30904  cdlemg46  30924  cdlemk6  31026  cdlemki  31030  cdlemksv2  31036  cdlemk11  31038  cdlemk6u  31051  cdleml4N  31168  cdlemn11pre  31400
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