![]() |
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 453 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
3 | 2 | an32s 631 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 |
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 197 df-an 383 |
This theorem is referenced by: sossfld 5720 infunsdom 9242 creui 11221 qreccl 12016 fsumrlim 14750 fsumo1 14751 climfsum 14759 imasvscaf 16407 grppropd 17645 grpinvpropd 17698 cycsubgcl 17828 frgpup1 18395 ringrghm 18813 phlpropd 20217 mamuass 20425 iccpnfcnv 22963 mbfeqalem 23629 mbfinf 23652 mbflimsup 23653 mbflimlem 23654 itgfsum 23813 plypf1 24188 mtest 24378 rpvmasum2 25422 ifeqeqx 29699 ordtconnlem1 30310 xrge0iifcnv 30319 fsum2dsub 31025 incsequz 33874 equivtotbnd 33907 intidl 34158 keridl 34161 prnc 34196 cdleme50trn123 36362 dva1dim 36793 dia1dim2 36870 |
Copyright terms: Public domain | W3C validator |