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 ⊢ (𝜑 ↔ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  2false  378  equsexvw  2037  cbvexv1  2371  cbvex2v  2373  cbvex  2428  cbvex2  2441  rexcom  3291  cbvrexfw  3303  ceqsex  3497  ceqsexv  3498  gencbval  3508  ceqsralbv  3610  snnzb  4675  raldifsnb  4755  uni0b  4893  opab0  5529  tsna1  39185  ralopabb  44521