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  6582  omeu  6583  dfac12lem2  7770  xaddass2  10570  xpncan  10571  divdenle  12820  pockthlem  12952  znidomb  16515  ang180lem5  20111  isosctrlem3  20120  log2tlbnd  20241  xrge0addass  23329  xrge0npcan  23333  axcontlem8  24599  congmul  27054  jm2.25lem1  27091  jm2.26  27095  jm2.27a  27098  4atexlemntlpq  30257  4atexlemnclw  30259  trlval2  30352  cdleme0moN  30414  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme17c  30477  cdlemeda  30487  cdleme20h  30505  cdleme20j  30507  cdleme20l2  30510  cdleme21c  30516  cdleme21ct  30518  cdleme22aa  30528  cdleme22cN  30531  cdleme22d  30532  cdleme22e  30533  cdleme22eALTN  30534  cdleme23b  30539  cdleme25a  30542  cdleme25dN  30545  cdleme27N  30558  cdleme28a  30559  cdleme28b  30560  cdleme29ex  30563  cdleme32c  30632  cdleme42k  30673  cdlemg2cex  30780  cdlemg2idN  30785  cdlemg31c  30888  cdlemk5a  31024  cdlemk5  31025
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