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  5120  infunsdom  7840  creui  9741  qreccl  10336  fsumrlim  12269  fsumo1  12270  climfsum  12278  imasvscaf  13441  grppropd  14500  grpinvpropd  14543  cycsubgcl  14643  frgpup1  15084  rngrghm  15389  phlpropd  16559  iccpnfcnv  18442  mbfeqalem  18997  mbfinf  19020  mbflimsup  19021  mbflimlem  19022  itgfsum  19181  plypf1  19594  mtest  19781  rpvmasum2  20661  isgrp2d  20902  sspival  21314  xrge0iifcnv  23315  incsequz  26458  equivtotbnd  26502  intidl  26654  keridl  26657  prnc  26692  mamuass  27460  cdleme50trn123  30743  dva1dim  31174  dia1dim2  31252
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