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  3079  pntrmax  20713  limptlimpr2lem1  25574  paddasslem4  30012  4atexlemu  30253  4atexlemv  30254  cdleme20aN  30498  cdleme20g  30504  cdlemg9a  30821  cdlemg12a  30832  cdlemg17dALTN  30853  cdlemg18b  30868  cdlemg18c  30869
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