Theorem con4bii 297

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

Hypothesis

Ref	Expression
con4bii.1

Assertion

Ref	Expression
con4bii

Proof of Theorem con4bii

Step	Hyp	Ref	Expression
1		con4bii.1	. 2
2		notbi 295	. 2
3	1, 2	mpbir 209	1

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

This theorem is referenced by:  2false  350  19.35OLD  1688  2ralor  3027  gencbval  3155  eq0  3800  snnzb  4094  raldifsnb  4161  uni0b  4274  tsna1  30551

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 185