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

Theorem anass1rs 807
Description: Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.)
Hypothesis
Ref Expression
anass1rs.1
Assertion
Ref Expression
anass1rs

Proof of Theorem anass1rs
StepHypRef Expression
1 anass1rs.1 . . 3
21anassrs 648 . 2
32an32s 804 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  sossfld  5459  infunsdom  8615  creui  10556  qreccl  11231  fsumrlim  13625  fsumo1  13626  climfsum  13634  imasvscaf  14936  grppropd  16068  grpinvpropd  16113  cycsubgcl  16227  frgpup1  16793  ringrghm  17251  phlpropd  18690  mamuass  18904  iccpnfcnv  21444  mbfeqalem  22049  mbfinf  22072  mbflimsup  22073  mbflimlem  22074  itgfsum  22233  plypf1  22609  mtest  22799  rpvmasum2  23697  isgrp2d  25237  sspival  25651  ifeqeqx  27419  ordtconlem1  27906  xrge0iifcnv  27915  incsequz  30241  equivtotbnd  30274  intidl  30426  keridl  30429  prnc  30464  cdleme50trn123  36280  dva1dim  36711  dia1dim2  36789
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
  Copyright terms: Public domain W3C validator