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  2007  cbvexv1  2346  cbvex2v  2348  cbvex  2403  cbvex2  2416  rexcom  3266  cbvrexfw  3278  ceqsex  3477  ceqsexv  3478  gencbval  3489  ceqsralbv  3599  snnzb  4662  raldifsnb  4741  uni0b  4876  opab0  5509  tsna1  38465  ralopabb  43838