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

Theorem anass1rs 798
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 641 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
32an32s 795 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  sossfld  5273  infunsdom  8371  creui  10304  qreccl  10960  fsumrlim  13256  fsumo1  13257  climfsum  13265  imasvscaf  14459  grppropd  15535  grpinvpropd  15580  cycsubgcl  15686  frgpup1  16251  rngrghm  16628  phlpropd  17925  mamuass  18147  iccpnfcnv  20357  mbfeqalem  20961  mbfinf  20984  mbflimsup  20985  mbflimlem  20986  itgfsum  21145  plypf1  21564  mtest  21753  rpvmasum2  22645  isgrp2d  23544  sspival  23958  ifeqeqx  25725  ordtconlem1  26207  xrge0iifcnv  26216  incsequz  28485  equivtotbnd  28518  intidl  28670  keridl  28673  prnc  28708  cdleme50trn123  33768  dva1dim  34199  dia1dim2  34277
  Copyright terms: Public domain W3C validator