Theorem con4bii 320

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 318	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
3	1, 2	mpbir 230	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  2false  375  equsexvw  2008  cbvexv1  2338  cbvex2v  2340  cbvex  2398  cbvex2  2411  2ralorOLD  3229  rexcom  3287  cbvrexfw  3302  ceqsex  3523  ceqsexv  3525  gencbval  3537  ceqsralbv  3645  snnzb  4722  raldifsnb  4799  uni0b  4937  opab0  5554  tsna1  37007  ralopabb  42152