Theorem con4bii 322

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

Syntax hints:  ¬ wn 3   ↔ wb 207

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 208

This theorem is referenced by:  2false  376  equsexvw  2012  cbvexv1  2350  cbvex2v  2352  cbvex  2407  cbvex2  2420  rexcom  3268  cbvrexfw  3280  ceqsex  3478  ceqsexv  3479  gencbval  3490  ceqsralbv  3595  snnzb  4650  raldifsnb  4729  uni0b  4864  opab0  5496  tsna1  38511  ralopabb  43855