Proof of Theorem anxordi
Step | Hyp | Ref
| Expression |
1 | | simpl 102 |
. 2
⊢ ((φ ∧ (ψ ⊻ χ)) → φ) |
2 | | df-xor 1266 |
. . . 4
⊢ (((φ ∧ ψ) ⊻ (φ ∧ χ)) ↔ (((φ ∧ ψ) ∨ (φ ∧ χ)) ∧ ¬
((φ ∧
ψ) ∧
(φ ∧
χ)))) |
3 | 2 | simplbi 259 |
. . 3
⊢ (((φ ∧ ψ) ⊻ (φ ∧ χ)) → ((φ ∧ ψ) ∨ (φ ∧ χ))) |
4 | | simpl 102 |
. . . 4
⊢ ((φ ∧ ψ) → φ) |
5 | | simpl 102 |
. . . 4
⊢ ((φ ∧ χ) → φ) |
6 | 4, 5 | jaoi 635 |
. . 3
⊢ (((φ ∧ ψ) ∨ (φ ∧ χ)) → φ) |
7 | 3, 6 | syl 14 |
. 2
⊢ (((φ ∧ ψ) ⊻ (φ ∧ χ)) → φ) |
8 | | ibar 285 |
. . 3
⊢ (φ → ((ψ ⊻ χ) ↔ (φ ∧ (ψ ⊻ χ)))) |
9 | | ibar 285 |
. . . 4
⊢ (φ → (ψ ↔ (φ ∧ ψ))) |
10 | | ibar 285 |
. . . 4
⊢ (φ → (χ ↔ (φ ∧ χ))) |
11 | 9, 10 | xorbi12d 1271 |
. . 3
⊢ (φ → ((ψ ⊻ χ) ↔ ((φ ∧ ψ) ⊻ (φ ∧ χ)))) |
12 | 8, 11 | bitr3d 179 |
. 2
⊢ (φ → ((φ ∧ (ψ ⊻ χ)) ↔ ((φ ∧ ψ) ⊻ (φ ∧ χ)))) |
13 | 1, 7, 12 | pm5.21nii 619 |
1
⊢ ((φ ∧ (ψ ⊻ χ)) ↔ ((φ ∧ ψ) ⊻ (φ ∧ χ))) |