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  2040  cbvexv1  2375  cbvex2v  2377  cbvex  2431  cbvex2  2444  rexcom  3295  cbvrexfw  3307  ceqsex  3501  ceqsexv  3502  gencbval  3512  ceqsralbv  3614  snnzb  4681  raldifsnb  4761  uni0b  4899  opab0  5536  tsna1  39342  ralopabb  44673