Theorem con4bii 324

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

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  2false  378  equsexvw  2035  cbvexv1  2374  cbvex2v  2376  cbvex  2431  cbvex2  2444  rexcom  3294  cbvrexfw  3306  ceqsex  3502  ceqsexv  3503  gencbval  3513  ceqsralbv  3616  snnzb  4684  raldifsnb  4764  uni0b  4899  opab0  5539  tsna1  38793  ralopabb  44137