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

Theorem anass1rs 783
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 630 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
32an32s 780 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  sossfld  5317  infunsdom  8094  creui  9995  qreccl  10594  fsumrlim  12590  fsumo1  12591  climfsum  12599  imasvscaf  13764  grppropd  14823  grpinvpropd  14866  cycsubgcl  14966  frgpup1  15407  rngrghm  15712  phlpropd  16886  iccpnfcnv  18969  mbfeqalem  19534  mbfinf  19557  mbflimsup  19558  mbflimlem  19559  itgfsum  19718  plypf1  20131  mtest  20320  rpvmasum2  21206  isgrp2d  21823  sspival  22237  ifeqeqx  24001  xrge0iifcnv  24319  incsequz  26452  equivtotbnd  26487  intidl  26639  keridl  26642  prnc  26677  mamuass  27437  cdleme50trn123  31351  dva1dim  31782  dia1dim2  31860
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator