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

Theorem anass1rs 782
Description: Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.)
Hypothesis
Ref Expression
anass1rs.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
anass1rs  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )

Proof of Theorem anass1rs
StepHypRef Expression
1 anass1rs.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21anassrs 629 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
32an32s 779 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sossfld  5136  infunsdom  7856  creui  9757  qreccl  10352  fsumrlim  12285  fsumo1  12286  climfsum  12294  imasvscaf  13457  grppropd  14516  grpinvpropd  14559  cycsubgcl  14659  frgpup1  15100  rngrghm  15405  phlpropd  16575  iccpnfcnv  18458  mbfeqalem  19013  mbfinf  19036  mbflimsup  19037  mbflimlem  19038  itgfsum  19197  plypf1  19610  mtest  19797  rpvmasum2  20677  isgrp2d  20918  sspival  21330  xrge0iifcnv  23330  incsequz  26561  equivtotbnd  26605  intidl  26757  keridl  26760  prnc  26795  mamuass  27563  cdleme50trn123  31365  dva1dim  31796  dia1dim2  31874
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
  Copyright terms: Public domain W3C validator