![]() |
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 898 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | |
2 | olc 899 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | jaodan 985 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
4 | orc 898 | . . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒)) | |
5 | 4 | anim2i 610 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
6 | olc 899 | . . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒)) | |
7 | 6 | anim2i 610 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
8 | 5, 7 | jaoi 888 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
9 | 3, 8 | impbii 201 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 ∨ wo 878 |
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 199 df-an 387 df-or 879 |
This theorem is referenced by: andir 1036 anddi 1038 annotanannotOLD 1039 cadan 1722 indi 4103 indifdir 4113 unrab 4127 unipr 4671 uniun 4679 unopab 4951 xpundi 5404 difxp 5799 coundir 5878 imadif 6206 unpreima 6590 tpostpos 7637 elznn0nn 11718 faclbnd4lem4 13376 opsrtoslem1 19844 mbfmax 23815 fta1glem2 24325 ofmulrt 24436 lgsquadlem3 25520 difrab2 29876 ordtconnlem1 30504 ballotlemodife 31094 subfacp1lem6 31702 soseq 32282 nosep1o 32360 lineunray 32782 bj-ismooredr2 33581 poimirlem30 33976 itg2addnclem2 33998 lzunuz 38168 diophun 38174 rmydioph 38417 rp-isfinite6 38698 relexpxpmin 38843 andi3or 39153 clsk1indlem3 39174 zeoALTV 42404 |
Copyright terms: Public domain | W3C validator |