| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > anandi | Structured version Visualization version GIF version | ||
| Description: Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.) |
| Ref | Expression |
|---|---|
| anandi | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anidm 564 | . . 3 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑) | |
| 2 | 1 | anbi1i 624 | . 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) |
| 3 | an4 656 | . 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) | |
| 4 | 2, 3 | bitr3i 277 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ 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: anandi3 1102 an3andi 1484 2eu4 2655 inrab 4316 uniin 4931 xpco 6309 dfpo2 6316 fin 6788 fndmin 7065 wfrlem5OLD 8353 oaord 8585 nnaord 8657 ixpin 8963 isffth2 17963 fucinv 18021 setcinv 18135 rngcinv 20637 ringcinv 20671 unocv 21698 bldisj 24408 blin 24431 mbfmax 25684 mbfimaopnlem 25690 mbfaddlem 25695 i1faddlem 25728 i1fmullem 25729 lgsquadlem3 27426 numedglnl 29161 wlkeq 29652 ofpreima 32675 cntzun 33071 isunit2 33244 ordtconnlem1 33923 fneval 36353 mbfposadd 37674 anan 38230 exanres 38296 iss2 38345 1cossres 38430 prtlem70 38858 fz1eqin 42780 fgraphopab 43215 rngcinvALTV 48192 ringcinvALTV 48226 itsclc0b 48693 i0oii 48817 io1ii 48818 |
| Copyright terms: Public domain | W3C validator |