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  6598  omeu  6599  dfac12lem2  7786  xaddass2  10586  xpncan  10587  divdenle  12836  pockthlem  12968  znidomb  16531  ang180lem5  20127  isosctrlem3  20136  log2tlbnd  20257  xrge0addass  23344  xrge0npcan  23348  axcontlem8  24671  congmul  27157  jm2.25lem1  27194  jm2.26  27198  jm2.27a  27201  4atexlemntlpq  30879  4atexlemnclw  30881  trlval2  30974  cdleme0moN  31036  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme16e  31093  cdleme17c  31099  cdlemeda  31109  cdleme20h  31127  cdleme20j  31129  cdleme20l2  31132  cdleme21c  31138  cdleme21ct  31140  cdleme22aa  31150  cdleme22cN  31153  cdleme22d  31154  cdleme22e  31155  cdleme22eALTN  31156  cdleme23b  31161  cdleme25a  31164  cdleme25dN  31167  cdleme27N  31180  cdleme28a  31181  cdleme28b  31182  cdleme29ex  31185  cdleme32c  31254  cdleme42k  31295  cdlemg2cex  31402  cdlemg2idN  31407  cdlemg31c  31510  cdlemk5a  31646  cdlemk5  31647
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