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

Theorem syl133anc 1207
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 1134 . 2  |-  ( ph  ->  ( et  /\  ze  /\  si ) )
9 syl133anc.8 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  ( et  /\  ze  /\  si ) )  ->  rh )
101, 2, 3, 4, 8, 9syl131anc 1197 1  |-  ( ph  ->  rh )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  syl233anc  1213  cgrtr4d  25911  cgrtrand  25919  cgrtr3and  25921  cgrcoml  25922  cgrextendand  25935  segconeu  25937  btwnouttr2  25948  cgr3tr4  25978  cgrxfr  25981  btwnxfr  25982  lineext  26002  brofs2  26003  brifs2  26004  fscgr  26006  btwnconn1lem2  26014  btwnconn1lem4  26016  btwnconn1lem8  26020  btwnconn1lem11  26023  brsegle2  26035  seglecgr12im  26036  segletr  26040  outsidele  26058  dalem13  30410  2llnma1b  30520  cdlemblem  30527  cdlemb  30528  lhpexle3  30746  lhpat  30777  4atex2-0bOLDN  30813  cdlemd4  30935  cdleme14  31007  cdleme19b  31038  cdleme20f  31048  cdleme20j  31052  cdleme20k  31053  cdleme20l2  31055  cdleme20  31058  cdleme22a  31074  cdleme22e  31078  cdleme26e  31093  cdleme28  31107  cdleme38n  31198  cdleme41sn4aw  31209  cdleme41snaw  31210  cdlemg6c  31354  cdlemg6  31357  cdlemg8c  31363  cdlemg9  31368  cdlemg10a  31374  cdlemg12c  31379  cdlemg12d  31380  cdlemg18d  31415  cdlemg18  31416  cdlemg20  31419  cdlemg21  31420  cdlemg22  31421  cdlemg28a  31427  cdlemg33b0  31435  cdlemg28b  31437  cdlemg33a  31440  cdlemg33  31445  cdlemg34  31446  cdlemg36  31448  cdlemg38  31449  cdlemg46  31469  cdlemk6  31571  cdlemki  31575  cdlemksv2  31581  cdlemk11  31583  cdlemk6u  31596  cdleml4N  31713  cdlemn11pre  31945
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator