Theorem con4bii 321

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  2false  375  equsexvw  2006  cbvexv1  2342  cbvex2v  2344  cbvex  2399  cbvex2  2412  rexcom  3261  cbvrexfw  3273  ceqsex  3485  ceqsexv  3487  gencbval  3498  ceqsralbv  3612  snnzb  4671  raldifsnb  4748  uni0b  4885  opab0  5494  tsna1  38190  ralopabb  43450