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 568 | . . 3 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑) | |
2 | 1 | anbi1i 627 | . 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) |
3 | an4 656 | . 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) | |
4 | 2, 3 | bitr3i 280 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ 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: anandi3 1104 an3andi 1484 2eu4 2655 inrab 4226 uniin 4850 xpco 6157 fin 6604 fndmin 6870 wfrlem5 8064 oaord 8280 nnaord 8352 ixpin 8609 isffth2 17428 fucinv 17487 setcinv 17601 unocv 20647 bldisj 23301 blin 23324 mbfmax 24551 mbfimaopnlem 24557 mbfaddlem 24562 i1faddlem 24595 i1fmullem 24596 lgsquadlem3 26268 numedglnl 27240 wlkeq 27726 ofpreima 30727 cntzun 31044 ordtconnlem1 31593 dfpo2 33446 fneval 34283 mbfposadd 35566 anan 36121 exanres 36172 iss2 36221 1cossres 36294 prtlem70 36613 fz1eqin 40302 fgraphopab 40746 rngcinv 45220 rngcinvALTV 45232 ringcinv 45271 ringcinvALTV 45295 itsclc0b 45799 i0oii 45894 io1ii 45895 |
Copyright terms: Public domain | W3C validator |