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 471 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
3 | 2 | an32s 652 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: sossfld 6012 1stconst 7814 infunsdom 9707 creui 11704 qreccl 12444 fsumrlim 15252 fsumo1 15253 climfsum 15261 imasvscaf 16908 grppropd 18229 grpinvpropd 18285 cycsubgcl 18460 frgpup1 19012 ringrghm 19470 phlpropd 20464 mamuass 21146 iccpnfcnv 23689 mbfeqalem1 24386 mbfinf 24410 mbflimsup 24411 mbflimlem 24412 itgfsum 24571 plypf1 24953 mtest 25143 rpvmasum2 26240 ifeqeqx 30451 ordtconnlem1 31438 xrge0iifcnv 31447 fsum2dsub 32149 fvineqsneu 35194 pibt2 35200 incsequz 35518 equivtotbnd 35548 intidl 35799 keridl 35802 prnc 35837 cdleme50trn123 38180 dva1dim 38611 dia1dim2 38688 3factsumint1 39638 |
Copyright terms: Public domain | W3C validator |