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

Theorem syl133anc 1246
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 1171 . 2  |-  ( ph  ->  ( et  /\  ze  /\  si ) )
9 syl133anc.8 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  ( et  /\  ze  /\  si ) )  ->  rh )
101, 2, 3, 4, 8, 9syl131anc 1236 1  |-  ( ph  ->  rh )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 968
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 185  df-an 371  df-3an 970
This theorem is referenced by:  syl233anc  1252  mdetuni0  18883  cgrtr4d  29198  cgrtrand  29206  cgrtr3and  29208  cgrcoml  29209  cgrextendand  29222  segconeu  29224  btwnouttr2  29235  cgr3tr4  29265  cgrxfr  29268  btwnxfr  29269  lineext  29289  brofs2  29290  brifs2  29291  fscgr  29293  btwnconn1lem2  29301  btwnconn1lem4  29303  btwnconn1lem8  29307  btwnconn1lem11  29310  brsegle2  29322  seglecgr12im  29323  segletr  29327  outsidele  29345  dalem13  34347  2llnma1b  34457  cdlemblem  34464  cdlemb  34465  lhpexle3  34683  lhpat  34714  4atex2-0bOLDN  34750  cdlemd4  34872  cdleme14  34944  cdleme19b  34975  cdleme20f  34985  cdleme20j  34989  cdleme20k  34990  cdleme20l2  34992  cdleme20  34995  cdleme22a  35011  cdleme22e  35015  cdleme26e  35030  cdleme28  35044  cdleme38n  35135  cdleme41sn4aw  35146  cdleme41snaw  35147  cdlemg6c  35291  cdlemg6  35294  cdlemg8c  35300  cdlemg9  35305  cdlemg10a  35311  cdlemg12c  35316  cdlemg12d  35317  cdlemg18d  35352  cdlemg18  35353  cdlemg20  35356  cdlemg21  35357  cdlemg22  35358  cdlemg28a  35364  cdlemg33b0  35372  cdlemg28b  35374  cdlemg33a  35377  cdlemg33  35382  cdlemg34  35383  cdlemg36  35385  cdlemg38  35386  cdlemg46  35406  cdlemk6  35508  cdlemki  35512  cdlemksv2  35518  cdlemk11  35520  cdlemk6u  35533  cdleml4N  35650  cdlemn11pre  35882
  Copyright terms: Public domain W3C validator