![]() |
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 460 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
3 | 2 | an32s 643 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 |
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 199 df-an 386 |
This theorem is referenced by: sossfld 5797 1stconst 7502 infunsdom 9324 creui 11307 qreccl 12053 fsumrlim 14881 fsumo1 14882 climfsum 14890 imasvscaf 16514 grppropd 17753 grpinvpropd 17806 cycsubgcl 17933 frgpup1 18503 ringrghm 18921 phlpropd 20324 mamuass 20533 iccpnfcnv 23071 mbfeqalem1 23749 mbfinf 23773 mbflimsup 23774 mbflimlem 23775 itgfsum 23934 plypf1 24309 mtest 24499 rpvmasum2 25553 ifeqeqx 29879 ordtconnlem1 30486 xrge0iifcnv 30495 fsum2dsub 31205 incsequz 34031 equivtotbnd 34064 intidl 34315 keridl 34318 prnc 34353 cdleme50trn123 36575 dva1dim 37006 dia1dim2 37083 |
Copyright terms: Public domain | W3C validator |