Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > andi | GIF version |
Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
Ref | Expression |
---|---|
andi | ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orc 701 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | |
2 | olc 700 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | jaodan 786 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
4 | orc 701 | . . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒)) | |
5 | 4 | anim2i 339 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
6 | olc 700 | . . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒)) | |
7 | 6 | anim2i 339 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
8 | 5, 7 | jaoi 705 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
9 | 3, 8 | impbii 125 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∨ wo 697 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: andir 808 anddi 810 dcim 826 dcan 918 excxor 1356 sbequilem 1810 sborv 1862 r19.43 2587 indi 3318 difindiss 3325 unrab 3342 unipr 3745 uniun 3750 unopab 4002 xpundi 4590 coundir 5036 unpreima 5538 tpostpos 6154 elni2 7115 elznn0nn 9061 |
Copyright terms: Public domain | W3C validator |