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  3266  cbvrexfw  3279  ceqsex  3496  ceqsexv  3498  gencbval  3509  ceqsralbv  3623  snnzb  4682  raldifsnb  4760  uni0b  4897  opab0  5514  tsna1  38138  ralopabb  43400