Theorem wl-3xorbi123i

Description: Equivalence theorem for triple xor. Copy of hadbi123i . (Contributed by Mario Carneiro, 4-Sep-2016)

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

Proof

Step	Hyp	Ref	Expression
1		wl-3xorbii.1	|- ( ps <-> ch )
2		wl-3xorbii.2	|- ( th <-> ta )
3		wl-3xorbii.3	|- ( et <-> ze )
4	1	a1i	|- ( T. -> ( ps <-> ch ) )
5	2	a1i	|- ( T. -> ( th <-> ta ) )
6	3	a1i	|- ( T. -> ( et <-> ze ) )
7	4 5 6	wl-3xorbi123d	|- ( T. -> ( hadd ( ps , th , et ) <-> hadd ( ch , ta , ze ) ) )
8	7	mptru	|- ( hadd ( ps , th , et ) <-> hadd ( ch , ta , ze ) )