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

Theorem syl133anc 1241
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 1168 . 2  |-  ( ph  ->  ( et  /\  ze  /\  si ) )
9 syl133anc.8 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  ( et  /\  ze  /\  si ) )  ->  rh )
101, 2, 3, 4, 8, 9syl131anc 1231 1  |-  ( ph  ->  rh )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  syl233anc  1247  mdetuni0  18427  cgrtr4d  28016  cgrtrand  28024  cgrtr3and  28026  cgrcoml  28027  cgrextendand  28040  segconeu  28042  btwnouttr2  28053  cgr3tr4  28083  cgrxfr  28086  btwnxfr  28087  lineext  28107  brofs2  28108  brifs2  28109  fscgr  28111  btwnconn1lem2  28119  btwnconn1lem4  28121  btwnconn1lem8  28125  btwnconn1lem11  28128  brsegle2  28140  seglecgr12im  28141  segletr  28145  outsidele  28163  dalem13  33320  2llnma1b  33430  cdlemblem  33437  cdlemb  33438  lhpexle3  33656  lhpat  33687  4atex2-0bOLDN  33723  cdlemd4  33845  cdleme14  33917  cdleme19b  33948  cdleme20f  33958  cdleme20j  33962  cdleme20k  33963  cdleme20l2  33965  cdleme20  33968  cdleme22a  33984  cdleme22e  33988  cdleme26e  34003  cdleme28  34017  cdleme38n  34108  cdleme41sn4aw  34119  cdleme41snaw  34120  cdlemg6c  34264  cdlemg6  34267  cdlemg8c  34273  cdlemg9  34278  cdlemg10a  34284  cdlemg12c  34289  cdlemg12d  34290  cdlemg18d  34325  cdlemg18  34326  cdlemg20  34329  cdlemg21  34330  cdlemg22  34331  cdlemg28a  34337  cdlemg33b0  34345  cdlemg28b  34347  cdlemg33a  34350  cdlemg33  34355  cdlemg34  34356  cdlemg36  34358  cdlemg38  34359  cdlemg46  34379  cdlemk6  34481  cdlemki  34485  cdlemksv2  34491  cdlemk11  34493  cdlemk6u  34506  cdleml4N  34623  cdlemn11pre  34855
  Copyright terms: Public domain W3C validator