![]() |
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 469 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
3 | 2 | an32s 651 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: sossfld 6183 1stconst 8083 infunsdom 10206 creui 12204 qreccl 12950 fsumrlim 15754 fsumo1 15755 climfsum 15763 imasvscaf 17482 grppropd 18834 grpinvpropd 18895 cycsubgcl 19078 frgpup1 19638 ringrghm 20119 phlpropd 21200 mamuass 21894 iccpnfcnv 24452 mbfeqalem1 25150 mbfinf 25174 mbflimsup 25175 mbflimlem 25176 itgfsum 25336 plypf1 25718 mtest 25908 rpvmasum2 27005 ifeqeqx 31762 ordtconnlem1 32893 xrge0iifcnv 32902 fsum2dsub 33608 fvineqsneu 36281 pibt2 36287 incsequz 36605 equivtotbnd 36635 intidl 36886 keridl 36889 prnc 36924 cdleme50trn123 39414 dva1dim 39845 dia1dim2 39922 3factsumint1 40875 |
Copyright terms: Public domain | W3C validator |