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

Theorem anass1rs 808
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 646 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
32an32s 805 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  sossfld  5270  infunsdom  8625  creui  10570  qreccl  11246  fsumrlim  13774  fsumo1  13775  climfsum  13783  imasvscaf  15151  grppropd  16390  grpinvpropd  16435  cycsubgcl  16549  frgpup1  17115  ringrghm  17569  phlpropd  18986  mamuass  19194  iccpnfcnv  21734  mbfeqalem  22339  mbfinf  22362  mbflimsup  22363  mbflimlem  22364  itgfsum  22523  plypf1  22899  mtest  23089  rpvmasum2  24076  isgrp2d  25637  sspival  26051  ifeqeqx  27826  ordtconlem1  28345  xrge0iifcnv  28354  incsequz  31503  equivtotbnd  31536  intidl  31688  keridl  31691  prnc  31726  cdleme50trn123  33553  dva1dim  33984  dia1dim2  34062
  Copyright terms: Public domain W3C validator