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

Theorem syl222anc 1200
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 519 . 2  |-  ( ph  ->  ( et  /\  ze ) )
8 syl222anc.7 . 2  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta )  /\  ( et  /\  ze ) )  ->  si )
91, 2, 3, 4, 7, 8syl221anc 1195 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3anandis  1285  3anandirs  1286  omopth2  6819  omeu  6820  dfac12lem2  8016  xaddass2  10821  xpncan  10822  divdenle  13133  pockthlem  13265  znidomb  16834  ang180lem5  20647  isosctrlem3  20656  log2tlbnd  20777  xlt2addrd  24116  xrge0addass  24203  xrge0npcan  24208  axcontlem8  25902  congmul  27023  jm2.25lem1  27060  jm2.26  27064  jm2.27a  27067  stoweidlem42  27758  4atexlemntlpq  30802  4atexlemnclw  30804  trlval2  30897  cdleme0moN  30959  cdleme16b  31013  cdleme16c  31014  cdleme16d  31015  cdleme16e  31016  cdleme17c  31022  cdlemeda  31032  cdleme20h  31050  cdleme20j  31052  cdleme20l2  31055  cdleme21c  31061  cdleme21ct  31063  cdleme22aa  31073  cdleme22cN  31076  cdleme22d  31077  cdleme22e  31078  cdleme22eALTN  31079  cdleme23b  31084  cdleme25a  31087  cdleme25dN  31090  cdleme27N  31103  cdleme28a  31104  cdleme28b  31105  cdleme29ex  31108  cdleme32c  31177  cdleme42k  31218  cdlemg2cex  31325  cdlemg2idN  31330  cdlemg31c  31433  cdlemk5a  31569  cdlemk5  31570
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator