| 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 868 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | |
| 2 | olc 869 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | |
| 3 | 1, 2 | jaodan 960 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
| 4 | orc 868 | . . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒)) | |
| 5 | 4 | anim2i 617 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
| 6 | olc 869 | . . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒)) | |
| 7 | 6 | anim2i 617 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
| 8 | 5, 7 | jaoi 858 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
| 9 | 3, 8 | impbii 209 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∨ wo 848 |
| 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 df-or 849 |
| This theorem is referenced by: andir 1011 anddi 1013 cadan 1609 indi 4284 unrab 4315 uniun 4930 unopab 5224 xpundi 5754 difxp 6184 coundir 6268 imadif 6650 unpreima 7083 soseq 8184 tpostpos 8271 elznn0nn 12627 faclbnd4lem4 14335 opsrtoslem1 22079 mbfmax 25684 fta1glem2 26208 ofmulrt 26323 lgsquadlem3 27426 nogesgn1o 27718 nosep1o 27726 noinfbnd2lem1 27775 difrab2 32517 ordtconnlem1 33923 ballotlemodife 34500 subfacp1lem6 35190 satf0op 35382 lineunray 36148 wl-ifpimpr 37467 wl-df2-3mintru2 37486 poimirlem30 37657 itg2addnclem2 37679 sticksstones22 42169 lzunuz 42779 diophun 42784 rmydioph 43026 fzunt 43468 fzuntd 43469 fzunt1d 43470 fzuntgd 43471 rp-isfinite6 43531 relexpxpmin 43730 andi3or 44037 clsk1indlem3 44056 simpcntrab 46885 zeoALTV 47657 |
| Copyright terms: Public domain | W3C validator |