Theorem con4bii 323

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  2false  377  equsexvw  2024  cbvexv1  2372  cbvex2v  2374  cbvex  2429  cbvex2  2442  rexcom  3290  cbvrexfw  3302  ceqsex  3500  ceqsexv  3501  gencbval  3511  ceqsralbv  3615  snnzb  4674  raldifsnb  4753  uni0b  4889  opab0  5521  tsna1  38604  ralopabb  43948