![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anass1rs | Structured version Visualization version GIF 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 467 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
3 | 2 | an32s 652 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 |
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 207 df-an 396 |
This theorem is referenced by: sossfld 6208 1stconst 8124 infunsdom 10251 creui 12259 qreccl 13009 fsumrlim 15844 fsumo1 15845 climfsum 15853 imasvscaf 17586 grppropd 18982 grpinvpropd 19046 cycsubgcl 19237 frgpup1 19808 ringrghm 20327 phlpropd 21691 mamuass 22422 iccpnfcnv 24989 mbfeqalem1 25690 mbfinf 25714 mbflimsup 25715 mbflimlem 25716 itgfsum 25877 plypf1 26266 mtest 26462 rpvmasum2 27571 ifeqeqx 32563 ordtconnlem1 33885 xrge0iifcnv 33894 fsum2dsub 34601 fvineqsneu 37394 pibt2 37400 incsequz 37735 equivtotbnd 37765 intidl 38016 keridl 38019 prnc 38054 cdleme50trn123 40537 dva1dim 40968 dia1dim2 41045 3factsumint1 42003 |
Copyright terms: Public domain | W3C validator |