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  5386  infunsdom  8487  creui  10421  qreccl  11077  fsumrlim  13385  fsumo1  13386  climfsum  13394  imasvscaf  14588  grppropd  15667  grpinvpropd  15712  cycsubgcl  15818  frgpup1  16385  rngrghm  16809  phlpropd  18202  mamuass  18424  iccpnfcnv  20641  mbfeqalem  21246  mbfinf  21269  mbflimsup  21270  mbflimlem  21271  itgfsum  21430  plypf1  21806  mtest  21995  rpvmasum2  22887  isgrp2d  23867  sspival  24281  ifeqeqx  26047  ordtconlem1  26492  xrge0iifcnv  26501  incsequz  28785  equivtotbnd  28818  intidl  28970  keridl  28973  prnc  29008  cdleme50trn123  34507  dva1dim  34938  dia1dim2  35016
  Copyright terms: Public domain W3C validator