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  2005  cbvexv1  2340  cbvex2v  2342  cbvex  2397  cbvex2  2410  rexcom  3258  cbvrexfw  3271  ceqsex  3487  ceqsexv  3489  gencbval  3500  ceqsralbv  3614  snnzb  4672  raldifsnb  4750  uni0b  4887  opab0  5501  tsna1  38126  ralopabb  43387