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 665 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | |
2 | olc 664 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | jaodan 743 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
4 | orc 665 | . . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒)) | |
5 | 4 | anim2i 334 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
6 | olc 664 | . . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒)) | |
7 | 6 | anim2i 334 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
8 | 5, 7 | jaoi 668 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒))) |
9 | 3, 8 | impbii 124 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 ∨ wo 661 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 662 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: andir 765 anddi 767 dcim 817 dcan 875 excxor 1309 sbequilem 1759 sborv 1811 r19.43 2512 indi 3211 difindiss 3218 unrab 3235 unipr 3615 uniun 3620 unopab 3857 xpundi 4414 coundir 4843 unpreima 5313 tpostpos 5902 elni2 6504 elznn0nn 8365 |
Copyright terms: Public domain | W3C validator |