Theorem xchbinx

Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014)

	Ref	Expression
Hypotheses	xchbinx.1	|- ( ph <-> -. ps )
	xchbinx.2	|- ( ps <-> ch )
Assertion	xchbinx	|- ( ph <-> -. ch )

Proof

Step	Hyp	Ref	Expression
1		xchbinx.1	|- ( ph <-> -. ps )
2		xchbinx.2	|- ( ps <-> ch )
3	2	notbii	|- ( -. ps <-> -. ch )
4	1 3	bitri	|- ( ph <-> -. ch )