MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl222anc 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  6763  omeu  6764  dfac12lem2  7957  xaddass2  10761  xpncan  10762  divdenle  13068  pockthlem  13200  znidomb  16765  ang180lem5  20522  isosctrlem3  20531  log2tlbnd  20652  xlt2addrd  23960  xrge0addass  24040  xrge0npcan  24045  axcontlem8  25624  congmul  26723  jm2.25lem1  26760  jm2.26  26764  jm2.27a  26767  stoweidlem42  27459  4atexlemntlpq  30182  4atexlemnclw  30184  trlval2  30277  cdleme0moN  30339  cdleme16b  30393  cdleme16c  30394  cdleme16d  30395  cdleme16e  30396  cdleme17c  30402  cdlemeda  30412  cdleme20h  30430  cdleme20j  30432  cdleme20l2  30435  cdleme21c  30441  cdleme21ct  30443  cdleme22aa  30453  cdleme22cN  30456  cdleme22d  30457  cdleme22e  30458  cdleme22eALTN  30459  cdleme23b  30464  cdleme25a  30467  cdleme25dN  30470  cdleme27N  30483  cdleme28a  30484  cdleme28b  30485  cdleme29ex  30488  cdleme32c  30557  cdleme42k  30598  cdlemg2cex  30705  cdlemg2idN  30710  cdlemg31c  30813  cdlemk5a  30949  cdlemk5  30950
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