This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xorbi12i

Description: Equality property for exclusive disjunction. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 21-Apr-2024)

	Ref	Expression
Hypotheses	xorbi12.1	$⊢ φ \leftrightarrow ψ$
	xorbi12.2	$⊢ χ \leftrightarrow θ$
Assertion	xorbi12i	$⊢ (φ ⊻ χ) \leftrightarrow (ψ ⊻ θ)$

Proof

Step	Hyp	Ref	Expression
1		xorbi12.1	$⊢ φ \leftrightarrow ψ$
2		xorbi12.2	$⊢ χ \leftrightarrow θ$
3		df-xor	$⊢ (φ ⊻ χ) \leftrightarrow \neg (φ \leftrightarrow χ)$
4	1 2	bibi12i	$⊢ (φ \leftrightarrow χ) \leftrightarrow (ψ \leftrightarrow θ)$
5	3 4	xchbinx	$⊢ (φ ⊻ χ) \leftrightarrow \neg (ψ \leftrightarrow θ)$
6		df-xor	$⊢ (ψ ⊻ θ) \leftrightarrow \neg (ψ \leftrightarrow θ)$
7	5 6	bitr4i	$⊢ (φ ⊻ χ) \leftrightarrow (ψ ⊻ θ)$