Theorem wl-3xorbi123d

Description: Equivalence theorem for triple xor. (Contributed by Mario Carneiro, 4-Sep-2016) df-had redefined. (Revised by Wolf Lammen, 24-Apr-2024)

	Ref	Expression
Hypotheses	wl-3xorbid.1	|- ( ph -> ( ps <-> ch ) )
	wl-3xorbid.2	|- ( ph -> ( th <-> ta ) )
	wl-3xorbid.3	|- ( ph -> ( et <-> ze ) )
Assertion	wl-3xorbi123d	|- ( ph -> ( hadd ( ps , th , et ) <-> hadd ( ch , ta , ze ) ) )

Proof

Step	Hyp	Ref	Expression
1		wl-3xorbid.1	|- ( ph -> ( ps <-> ch ) )
2		wl-3xorbid.2	|- ( ph -> ( th <-> ta ) )
3		wl-3xorbid.3	|- ( ph -> ( et <-> ze ) )
4	1 2	bibi12d	|- ( ph -> ( ( ps <-> th ) <-> ( ch <-> ta ) ) )
5	4 3	bibi12d	|- ( ph -> ( ( ( ps <-> th ) <-> et ) <-> ( ( ch <-> ta ) <-> ze ) ) )
6		wl-3xorbi2	|- ( hadd ( ps , th , et ) <-> ( ( ps <-> th ) <-> et ) )
7		wl-3xorbi2	|- ( hadd ( ch , ta , ze ) <-> ( ( ch <-> ta ) <-> ze ) )
8	5 6 7	3bitr4g	|- ( ph -> ( hadd ( ps , th , et ) <-> hadd ( ch , ta , ze ) ) )