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

Theorem syl133anc 1315
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1  |-  ( ph  ->  ps )
syl12anc.2  |-  ( ph  ->  ch )
syl12anc.3  |-  ( ph  ->  th )
syl22anc.4  |-  ( ph  ->  ta )
syl23anc.5  |-  ( ph  ->  et )
syl33anc.6  |-  ( ph  ->  ze )
syl133anc.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 syl12anc.1 . 2  |-  ( ph  ->  ps )
2 syl12anc.2 . 2  |-  ( ph  ->  ch )
3 syl12anc.3 . 2  |-  ( ph  ->  th )
4 syl22anc.4 . 2  |-  ( ph  ->  ta )
5 syl23anc.5 . . 3  |-  ( ph  ->  et )
6 syl33anc.6 . . 3  |-  ( ph  ->  ze )
7 syl133anc.7 . . 3  |-  ( ph  ->  si )
85, 6, 73jca 1210 . 2  |-  ( ph  ->  ( et  /\  ze  /\  si ) )
9 syl133anc.8 . 2  |-  ( ( ps  /\  ( ch 
/\  th  /\  ta )  /\  ( et  /\  ze  /\  si ) )  ->  rh )
101, 2, 3, 4, 8, 9syl131anc 1305 1  |-  ( ph  ->  rh )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  syl233anc  1321  mdetuni0  19723  cgrtr4d  30823  cgrtrand  30831  cgrtr3and  30833  cgrcoml  30834  cgrextendand  30847  segconeu  30849  btwnouttr2  30860  cgr3tr4  30890  cgrxfr  30893  btwnxfr  30894  lineext  30914  brofs2  30915  brifs2  30916  fscgr  30918  btwnconn1lem2  30926  btwnconn1lem4  30928  btwnconn1lem8  30932  btwnconn1lem11  30935  brsegle2  30947  seglecgr12im  30948  segletr  30952  outsidele  30970  dalem13  33312  2llnma1b  33422  cdlemblem  33429  cdlemb  33430  lhpexle3  33648  lhpat  33679  4atex2-0bOLDN  33715  cdlemd4  33838  cdleme14  33910  cdleme19b  33942  cdleme20f  33952  cdleme20j  33956  cdleme20k  33957  cdleme20l2  33959  cdleme20  33962  cdleme22a  33978  cdleme22e  33982  cdleme26e  33997  cdleme28  34011  cdleme38n  34102  cdleme41sn4aw  34113  cdleme41snaw  34114  cdlemg6c  34258  cdlemg6  34261  cdlemg8c  34267  cdlemg9  34272  cdlemg10a  34278  cdlemg12c  34283  cdlemg12d  34284  cdlemg18d  34319  cdlemg18  34320  cdlemg20  34323  cdlemg21  34324  cdlemg22  34325  cdlemg28a  34331  cdlemg33b0  34339  cdlemg28b  34341  cdlemg33a  34344  cdlemg33  34349  cdlemg34  34350  cdlemg36  34352  cdlemg38  34353  cdlemg46  34373  cdlemk6  34475  cdlemki  34479  cdlemksv2  34485  cdlemk11  34487  cdlemk6u  34500  cdleml4N  34617  cdlemn11pre  34849
  Copyright terms: Public domain W3C validator