|   | 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 467 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | 
| 3 | 2 | an32s 652 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: sossfld 6205 1stconst 8126 infunsdom 10254 creui 12262 qreccl 13012 fsumrlim 15848 fsumo1 15849 climfsum 15857 imasvscaf 17585 grppropd 18970 grpinvpropd 19034 cycsubgcl 19225 frgpup1 19794 ringrghm 20311 phlpropd 21674 mamuass 22407 iccpnfcnv 24976 mbfeqalem1 25677 mbfinf 25701 mbflimsup 25702 mbflimlem 25703 itgfsum 25863 plypf1 26252 mtest 26448 rpvmasum2 27557 ifeqeqx 32556 ordtconnlem1 33924 xrge0iifcnv 33933 fsum2dsub 34623 fvineqsneu 37413 pibt2 37419 incsequz 37756 equivtotbnd 37786 intidl 38037 keridl 38040 prnc 38075 cdleme50trn123 40557 dva1dim 40988 dia1dim2 41065 3factsumint1 42023 modelac8prim 45014 | 
| Copyright terms: Public domain | W3C validator |