![]() |
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 865 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | |
2 | olc 866 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | jaodan 955 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
4 | orc 865 | . . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒)) | |
5 | 4 | anim2i 615 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
6 | olc 866 | . . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒)) | |
7 | 6 | anim2i 615 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
8 | 5, 7 | jaoi 855 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
9 | 3, 8 | impbii 208 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 ∨ wo 845 |
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 395 df-or 846 |
This theorem is referenced by: andir 1006 anddi 1008 cadan 1602 indi 4272 indifdirOLD 4284 unrab 4304 uniprOLD 4927 uniun 4934 unopab 5231 xpundi 5746 difxp 6170 coundir 6254 imadif 6638 unpreima 7071 soseq 8164 tpostpos 8252 elznn0nn 12605 faclbnd4lem4 14291 opsrtoslem1 22021 mbfmax 25622 fta1glem2 26148 ofmulrt 26261 lgsquadlem3 27360 nogesgn1o 27652 nosep1o 27660 noinfbnd2lem1 27709 difrab2 32374 ordtconnlem1 33656 ballotlemodife 34248 subfacp1lem6 34926 satf0op 35118 lineunray 35874 wl-ifpimpr 37076 wl-df2-3mintru2 37095 poimirlem30 37254 itg2addnclem2 37276 sticksstones22 41771 lzunuz 42330 diophun 42335 rmydioph 42577 fzunt 43027 fzuntd 43028 fzunt1d 43029 fzuntgd 43030 rp-isfinite6 43090 relexpxpmin 43289 andi3or 43596 clsk1indlem3 43615 simpcntrab 46396 zeoALTV 47147 |
Copyright terms: Public domain | W3C validator |