![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anass1rs | Structured version Visualization version Unicode version |
Description: Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.) |
Ref | Expression |
---|---|
anass1rs.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
anass1rs |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anass1rs.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anassrs 654 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | an32s 813 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 189 df-an 373 |
This theorem is referenced by: sossfld 5283 infunsdom 8644 creui 10604 qreccl 11284 fsumrlim 13871 fsumo1 13872 climfsum 13880 imasvscaf 15445 grppropd 16684 grpinvpropd 16729 cycsubgcl 16843 frgpup1 17425 ringrghm 17833 phlpropd 19222 mamuass 19427 iccpnfcnv 21972 mbfeqalem 22598 mbfinf 22621 mbfinfOLD 22622 mbflimsup 22623 mbflimsupOLD 22624 mbflimlem 22625 itgfsum 22784 plypf1 23166 mtest 23359 rpvmasum2 24350 isgrp2d 25963 sspival 26377 ifeqeqx 28158 ordtconlem1 28730 xrge0iifcnv 28739 incsequz 32077 equivtotbnd 32110 intidl 32262 keridl 32265 prnc 32300 cdleme50trn123 34121 dva1dim 34552 dia1dim2 34630 |
Copyright terms: Public domain | W3C validator |