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

Theorem syl133anc 1250
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 1175 . 2  |-  ( ph  ->  ( et  /\  ze  /\  si ) )
9 syl133anc.8 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  ( et  /\  ze  /\  si ) )  ->  rh )
101, 2, 3, 4, 8, 9syl131anc 1240 1  |-  ( ph  ->  rh )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 972
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 974
This theorem is referenced by:  syl233anc  1256  mdetuni0  18990  cgrtr4d  29603  cgrtrand  29611  cgrtr3and  29613  cgrcoml  29614  cgrextendand  29627  segconeu  29629  btwnouttr2  29640  cgr3tr4  29670  cgrxfr  29673  btwnxfr  29674  lineext  29694  brofs2  29695  brifs2  29696  fscgr  29698  btwnconn1lem2  29706  btwnconn1lem4  29708  btwnconn1lem8  29712  btwnconn1lem11  29715  brsegle2  29727  seglecgr12im  29728  segletr  29732  outsidele  29750  dalem13  35102  2llnma1b  35212  cdlemblem  35219  cdlemb  35220  lhpexle3  35438  lhpat  35469  4atex2-0bOLDN  35505  cdlemd4  35628  cdleme14  35700  cdleme19b  35732  cdleme20f  35742  cdleme20j  35746  cdleme20k  35747  cdleme20l2  35749  cdleme20  35752  cdleme22a  35768  cdleme22e  35772  cdleme26e  35787  cdleme28  35801  cdleme38n  35892  cdleme41sn4aw  35903  cdleme41snaw  35904  cdlemg6c  36048  cdlemg6  36051  cdlemg8c  36057  cdlemg9  36062  cdlemg10a  36068  cdlemg12c  36073  cdlemg12d  36074  cdlemg18d  36109  cdlemg18  36110  cdlemg20  36113  cdlemg21  36114  cdlemg22  36115  cdlemg28a  36121  cdlemg33b0  36129  cdlemg28b  36131  cdlemg33a  36134  cdlemg33  36139  cdlemg34  36140  cdlemg36  36142  cdlemg38  36143  cdlemg46  36163  cdlemk6  36265  cdlemki  36269  cdlemksv2  36275  cdlemk11  36277  cdlemk6u  36290  cdleml4N  36407  cdlemn11pre  36639
  Copyright terms: Public domain W3C validator