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  2372  cbvex2v  2374  cbvex  2429  cbvex2  2442  rexcom  3292  cbvrexfw  3304  ceqsex  3498  ceqsexv  3499  gencbval  3509  ceqsralbv  3611  snnzb  4679  raldifsnb  4759  uni0b  4894  opab0  5529  tsna1  39056  ralopabb  44396