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  6584  omeu  6585  dfac12lem2  7772  xaddass2  10572  xpncan  10573  divdenle  12822  pockthlem  12954  znidomb  16517  ang180lem5  20113  isosctrlem3  20122  log2tlbnd  20243  xrge0addass  23331  xrge0npcan  23335  axcontlem8  24601  congmul  27065  jm2.25lem1  27102  jm2.26  27106  jm2.27a  27109  4atexlemntlpq  30330  4atexlemnclw  30332  trlval2  30425  cdleme0moN  30487  cdleme16b  30541  cdleme16c  30542  cdleme16d  30543  cdleme16e  30544  cdleme17c  30550  cdlemeda  30560  cdleme20h  30578  cdleme20j  30580  cdleme20l2  30583  cdleme21c  30589  cdleme21ct  30591  cdleme22aa  30601  cdleme22cN  30604  cdleme22d  30605  cdleme22e  30606  cdleme22eALTN  30607  cdleme23b  30612  cdleme25a  30615  cdleme25dN  30618  cdleme27N  30631  cdleme28a  30632  cdleme28b  30633  cdleme29ex  30636  cdleme32c  30705  cdleme42k  30746  cdlemg2cex  30853  cdlemg2idN  30858  cdlemg31c  30961  cdlemk5a  31097  cdlemk5  31098
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