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

Theorem anass1rs 805
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 648 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
32an32s 802 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  5280  infunsdom  8375  creui  10309  qreccl  10965  fsumrlim  13266  fsumo1  13267  climfsum  13275  imasvscaf  14469  grppropd  15547  grpinvpropd  15592  cycsubgcl  15698  frgpup1  16263  rngrghm  16682  phlpropd  18059  mamuass  18281  iccpnfcnv  20491  mbfeqalem  21095  mbfinf  21118  mbflimsup  21119  mbflimlem  21120  itgfsum  21279  plypf1  21655  mtest  21844  rpvmasum2  22736  isgrp2d  23673  sspival  24087  ifeqeqx  25853  ordtconlem1  26306  xrge0iifcnv  26315  incsequz  28597  equivtotbnd  28630  intidl  28782  keridl  28785  prnc  28820  cdleme50trn123  34038  dva1dim  34469  dia1dim2  34547
  Copyright terms: Public domain W3C validator