Theorem xchnxbir

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

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

Proof

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