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

Theorem syl212anc 1192
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 )
syl212anc.6  |-  ( ( ( ps  /\  ch )  /\  th  /\  ( ta  /\  et ) )  ->  ze )
Assertion
Ref Expression
syl212anc  |-  ( ph  ->  ze )

Proof of Theorem syl212anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . 2  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
5 sylXanc.5 . . 3  |-  ( ph  ->  et )
64, 5jca 518 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 syl212anc.6 . 2  |-  ( ( ( ps  /\  ch )  /\  th  /\  ( ta  /\  et ) )  ->  ze )
81, 2, 3, 6, 7syl211anc 1188 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  rmob  3092  pntrmax  20729  limptlimpr2lem1  25677  paddasslem4  30634  4atexlemu  30875  4atexlemv  30876  cdleme20aN  31120  cdleme20g  31126  cdlemg9a  31443  cdlemg12a  31454  cdlemg17dALTN  31475  cdlemg18b  31490  cdlemg18c  31491
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator