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  2038  cbvexv1  2376  cbvex2v  2378  cbvex  2433  cbvex2  2446  rexcom  3296  cbvrexfw  3308  ceqsex  3504  ceqsexv  3505  gencbval  3515  ceqsralbv  3618  snnzb  4686  raldifsnb  4766  uni0b  4901  opab0  5541  tsna1  38851  ralopabb  44195