![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > andi | Structured version Visualization version GIF version |
Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
Ref | Expression |
---|---|
andi | ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orc 866 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | |
2 | olc 867 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | jaodan 957 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
4 | orc 866 | . . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒)) | |
5 | 4 | anim2i 618 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
6 | olc 867 | . . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒)) | |
7 | 6 | anim2i 618 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
8 | 5, 7 | jaoi 856 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
9 | 3, 8 | impbii 208 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∨ wo 846 |
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 398 df-or 847 |
This theorem is referenced by: andir 1008 anddi 1010 cadan 1611 indi 4238 indifdirOLD 4250 unrab 4270 uniprOLD 4889 uniun 4896 unopab 5192 xpundi 5705 difxp 6121 coundir 6205 imadif 6590 unpreima 7018 soseq 8096 tpostpos 8182 elznn0nn 12520 faclbnd4lem4 14203 opsrtoslem1 21478 mbfmax 25029 fta1glem2 25547 ofmulrt 25658 lgsquadlem3 26746 nogesgn1o 27037 nosep1o 27045 noinfbnd2lem1 27094 difrab2 31468 ordtconnlem1 32545 ballotlemodife 33137 subfacp1lem6 33819 satf0op 34011 lineunray 34761 wl-ifpimpr 35966 wl-df2-3mintru2 35985 poimirlem30 36137 itg2addnclem2 36159 sticksstones22 40605 lzunuz 41120 diophun 41125 rmydioph 41367 fzunt 41801 fzuntd 41802 fzunt1d 41803 fzuntgd 41804 rp-isfinite6 41864 relexpxpmin 42063 andi3or 42370 clsk1indlem3 42389 simpcntrab 45185 zeoALTV 45936 |
Copyright terms: Public domain | W3C validator |