Theorem xorass

Description: The connector \/_ is associative. (Contributed by FL, 22-Nov-2010) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Proof shortened by Wolf Lammen, 20-Jun-2020)

	Ref	Expression
Assertion	xorass	|- ( ( ( ph \/_ ps ) \/_ ch ) <-> ( ph \/_ ( ps \/_ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		xor3	|- ( -. ( ph <-> ( ps \/_ ch ) ) <-> ( ph <-> -. ( ps \/_ ch ) ) )
2		biass	|- ( ( ( ph <-> ps ) <-> ch ) <-> ( ph <-> ( ps <-> ch ) ) )
3		xnor	|- ( ( ph <-> ps ) <-> -. ( ph \/_ ps ) )
4	3	bibi1i	|- ( ( ( ph <-> ps ) <-> ch ) <-> ( -. ( ph \/_ ps ) <-> ch ) )
5		xnor	|- ( ( ps <-> ch ) <-> -. ( ps \/_ ch ) )
6	5	bibi2i	|- ( ( ph <-> ( ps <-> ch ) ) <-> ( ph <-> -. ( ps \/_ ch ) ) )
7	2 4 6	3bitr3i	|- ( ( -. ( ph \/_ ps ) <-> ch ) <-> ( ph <-> -. ( ps \/_ ch ) ) )
8		nbbn	|- ( ( -. ( ph \/_ ps ) <-> ch ) <-> -. ( ( ph \/_ ps ) <-> ch ) )
9	1 7 8	3bitr2ri	|- ( -. ( ( ph \/_ ps ) <-> ch ) <-> -. ( ph <-> ( ps \/_ ch ) ) )
10		df-xor	|- ( ( ( ph \/_ ps ) \/_ ch ) <-> -. ( ( ph \/_ ps ) <-> ch ) )
11		df-xor	|- ( ( ph \/_ ( ps \/_ ch ) ) <-> -. ( ph <-> ( ps \/_ ch ) ) )
12	9 10 11	3bitr4i	|- ( ( ( ph \/_ ps ) \/_ ch ) <-> ( ph \/_ ( ps \/_ ch ) ) )