Theorem con4bii 311

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

Hypothesis

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

Assertion

Ref	Expression
con4bii	|- ( ph <-> ps )

Proof of Theorem con4bii

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

Syntax hints:   -. wn 3   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  2false  365  2ralor  3109  gencbval  3252  snnzb  4254  raldifsnb  4325  uni0b  4463  opab0  5007  ceqsralv2  31607  tsna1  33951