Theorem xchnxbi

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

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

Proof

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