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

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

Proof of Theorem syl222anc
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 )
75, 6jca 518 . 2  |-  ( ph  ->  ( et  /\  ze ) )
8 syl222anc.7 . 2  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta )  /\  ( et  /\  ze ) )  ->  si )
91, 2, 3, 4, 7, 8syl221anc 1193 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3anandis  1283  3anandirs  1284  omopth2  6578  omeu  6579  dfac12lem2  7766  xaddass2  10566  xpncan  10567  divdenle  12816  pockthlem  12948  znidomb  16511  ang180lem5  20107  isosctrlem3  20116  log2tlbnd  20237  axcontlem8  24009  congmul  26465  jm2.25lem1  26502  jm2.26  26506  jm2.27a  26509  4atexlemntlpq  29536  4atexlemnclw  29538  trlval2  29631  cdleme0moN  29693  cdleme16b  29747  cdleme16c  29748  cdleme16d  29749  cdleme16e  29750  cdleme17c  29756  cdlemeda  29766  cdleme20h  29784  cdleme20j  29786  cdleme20l2  29789  cdleme21c  29795  cdleme21ct  29797  cdleme22aa  29807  cdleme22cN  29810  cdleme22d  29811  cdleme22e  29812  cdleme22eALTN  29813  cdleme23b  29818  cdleme25a  29821  cdleme25dN  29824  cdleme27N  29837  cdleme28a  29838  cdleme28b  29839  cdleme29ex  29842  cdleme32c  29911  cdleme42k  29952  cdlemg2cex  30059  cdlemg2idN  30064  cdlemg31c  30167  cdlemk5a  30303  cdlemk5  30304
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