Description: Equality property for exclusive disjunction. (Contributed by Mario Carneiro, 4-Sep-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | xor12d.1 | ⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) | |
xor12d.2 | ⊢ ( 𝜑 → ( 𝜃 ↔ 𝜏 ) ) | ||
Assertion | xorbi12d | ⊢ ( 𝜑 → ( ( 𝜓 ⊻ 𝜃 ) ↔ ( 𝜒 ⊻ 𝜏 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xor12d.1 | ⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) | |
2 | xor12d.2 | ⊢ ( 𝜑 → ( 𝜃 ↔ 𝜏 ) ) | |
3 | 1 2 | bibi12d | ⊢ ( 𝜑 → ( ( 𝜓 ↔ 𝜃 ) ↔ ( 𝜒 ↔ 𝜏 ) ) ) |
4 | 3 | notbid | ⊢ ( 𝜑 → ( ¬ ( 𝜓 ↔ 𝜃 ) ↔ ¬ ( 𝜒 ↔ 𝜏 ) ) ) |
5 | df-xor | ⊢ ( ( 𝜓 ⊻ 𝜃 ) ↔ ¬ ( 𝜓 ↔ 𝜃 ) ) | |
6 | df-xor | ⊢ ( ( 𝜒 ⊻ 𝜏 ) ↔ ¬ ( 𝜒 ↔ 𝜏 ) ) | |
7 | 4 5 6 | 3bitr4g | ⊢ ( 𝜑 → ( ( 𝜓 ⊻ 𝜃 ) ↔ ( 𝜒 ⊻ 𝜏 ) ) ) |