![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anxordi | Structured version Visualization version GIF version |
Description: Conjunction distributes over exclusive-or. In intuitionistic logic this assertion is also true, even though xordi 1016 does not necessarily hold, in part because the usual definition of xor is subtly different in intuitionistic logic. (Contributed by David A. Wheeler, 7-Oct-2018.) |
Ref | Expression |
---|---|
anxordi | ⊢ ((𝜑 ∧ (𝜓 ⊻ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ⊻ (𝜑 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xordi 1016 | . 2 ⊢ ((𝜑 ∧ ¬ (𝜓 ↔ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))) | |
2 | df-xor 1511 | . . 3 ⊢ ((𝜓 ⊻ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒)) | |
3 | 2 | anbi2i 624 | . 2 ⊢ ((𝜑 ∧ (𝜓 ⊻ 𝜒)) ↔ (𝜑 ∧ ¬ (𝜓 ↔ 𝜒))) |
4 | df-xor 1511 | . 2 ⊢ (((𝜑 ∧ 𝜓) ⊻ (𝜑 ∧ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))) | |
5 | 1, 3, 4 | 3bitr4i 303 | 1 ⊢ ((𝜑 ∧ (𝜓 ⊻ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ⊻ (𝜑 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 397 ⊻ wxo 1510 |
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 398 df-xor 1511 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |