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  5452  infunsdom  8590  creui  10527  qreccl  11198  fsumrlim  13584  fsumo1  13585  climfsum  13593  imasvscaf  14790  grppropd  15869  grpinvpropd  15914  cycsubgcl  16022  frgpup1  16589  rngrghm  17035  phlpropd  18457  mamuass  18671  iccpnfcnv  21179  mbfeqalem  21784  mbfinf  21807  mbflimsup  21808  mbflimlem  21809  itgfsum  21968  plypf1  22344  mtest  22533  rpvmasum2  23425  isgrp2d  24913  sspival  25327  ifeqeqx  27093  ordtconlem1  27542  xrge0iifcnv  27551  incsequz  29844  equivtotbnd  29877  intidl  30029  keridl  30032  prnc  30067  cdleme50trn123  35350  dva1dim  35781  dia1dim2  35859
  Copyright terms: Public domain W3C validator