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

Theorem anass1rs 783
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 630 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
32an32s 780 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  sossfld  5276  infunsdom  8050  creui  9951  qreccl  10550  fsumrlim  12545  fsumo1  12546  climfsum  12554  imasvscaf  13719  grppropd  14778  grpinvpropd  14821  cycsubgcl  14921  frgpup1  15362  rngrghm  15667  phlpropd  16841  iccpnfcnv  18922  mbfeqalem  19487  mbfinf  19510  mbflimsup  19511  mbflimlem  19512  itgfsum  19671  plypf1  20084  mtest  20273  rpvmasum2  21159  isgrp2d  21776  sspival  22190  ifeqeqx  23954  xrge0iifcnv  24272  incsequz  26342  equivtotbnd  26377  intidl  26529  keridl  26532  prnc  26567  mamuass  27328  cdleme50trn123  31036  dva1dim  31467  dia1dim2  31545
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
  Copyright terms: Public domain W3C validator