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

Theorem syl133anc 1287
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 1185 . 2  |-  ( ph  ->  ( et  /\  ze  /\  si ) )
9 syl133anc.8 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  ( et  /\  ze  /\  si ) )  ->  rh )
101, 2, 3, 4, 8, 9syl131anc 1277 1  |-  ( ph  ->  rh )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  syl233anc  1293  mdetuni0  19630  cgrtr4d  30742  cgrtrand  30750  cgrtr3and  30752  cgrcoml  30753  cgrextendand  30766  segconeu  30768  btwnouttr2  30779  cgr3tr4  30809  cgrxfr  30812  btwnxfr  30813  lineext  30833  brofs2  30834  brifs2  30835  fscgr  30837  btwnconn1lem2  30845  btwnconn1lem4  30847  btwnconn1lem8  30851  btwnconn1lem11  30854  brsegle2  30866  seglecgr12im  30867  segletr  30871  outsidele  30889  dalem13  33157  2llnma1b  33267  cdlemblem  33274  cdlemb  33275  lhpexle3  33493  lhpat  33524  4atex2-0bOLDN  33560  cdlemd4  33683  cdleme14  33755  cdleme19b  33787  cdleme20f  33797  cdleme20j  33801  cdleme20k  33802  cdleme20l2  33804  cdleme20  33807  cdleme22a  33823  cdleme22e  33827  cdleme26e  33842  cdleme28  33856  cdleme38n  33947  cdleme41sn4aw  33958  cdleme41snaw  33959  cdlemg6c  34103  cdlemg6  34106  cdlemg8c  34112  cdlemg9  34117  cdlemg10a  34123  cdlemg12c  34128  cdlemg12d  34129  cdlemg18d  34164  cdlemg18  34165  cdlemg20  34168  cdlemg21  34169  cdlemg22  34170  cdlemg28a  34176  cdlemg33b0  34184  cdlemg28b  34186  cdlemg33a  34189  cdlemg33  34194  cdlemg34  34195  cdlemg36  34197  cdlemg38  34198  cdlemg46  34218  cdlemk6  34320  cdlemki  34324  cdlemksv2  34330  cdlemk11  34332  cdlemk6u  34345  cdleml4N  34462  cdlemn11pre  34694
  Copyright terms: Public domain W3C validator