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

Theorem anass1rs 816
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 654 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
32an32s 813 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  sossfld  5283  infunsdom  8644  creui  10604  qreccl  11284  fsumrlim  13871  fsumo1  13872  climfsum  13880  imasvscaf  15445  grppropd  16684  grpinvpropd  16729  cycsubgcl  16843  frgpup1  17425  ringrghm  17833  phlpropd  19222  mamuass  19427  iccpnfcnv  21972  mbfeqalem  22598  mbfinf  22621  mbfinfOLD  22622  mbflimsup  22623  mbflimsupOLD  22624  mbflimlem  22625  itgfsum  22784  plypf1  23166  mtest  23359  rpvmasum2  24350  isgrp2d  25963  sspival  26377  ifeqeqx  28158  ordtconlem1  28730  xrge0iifcnv  28739  incsequz  32077  equivtotbnd  32110  intidl  32262  keridl  32265  prnc  32300  cdleme50trn123  34121  dva1dim  34552  dia1dim2  34630
  Copyright terms: Public domain W3C validator