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 468 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
3 | 2 | an32s 649 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 397 |
This theorem is referenced by: sossfld 6094 1stconst 7949 infunsdom 9979 creui 11977 qreccl 12718 fsumrlim 15532 fsumo1 15533 climfsum 15541 imasvscaf 17259 grppropd 18603 grpinvpropd 18659 cycsubgcl 18834 frgpup1 19390 ringrghm 19853 phlpropd 20869 mamuass 21558 iccpnfcnv 24116 mbfeqalem1 24814 mbfinf 24838 mbflimsup 24839 mbflimlem 24840 itgfsum 25000 plypf1 25382 mtest 25572 rpvmasum2 26669 ifeqeqx 30894 ordtconnlem1 31883 xrge0iifcnv 31892 fsum2dsub 32596 fvineqsneu 35591 pibt2 35597 incsequz 35915 equivtotbnd 35945 intidl 36196 keridl 36199 prnc 36234 cdleme50trn123 38575 dva1dim 39006 dia1dim2 39083 3factsumint1 40036 |
Copyright terms: Public domain | W3C validator |