Theorem con4bii

Description: A contraposition inference. (Contributed by NM, 21-May-1994)

	Ref	Expression
Hypothesis	con4bii.1	|- ( -. ph <-> -. ps )
Assertion	con4bii	|- ( ph <-> ps )

Proof

Step	Hyp	Ref	Expression
1		con4bii.1	|- ( -. ph <-> -. ps )
2		notbi	|- ( ( ph <-> ps ) <-> ( -. ph <-> -. ps ) )
3	1 2	mpbir	|- ( ph <-> ps )