Theorem xchbinxr

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

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

Proof

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