Theorem con4bii 321

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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  2false  376  equsexvw  2009  cbvexv1  2339  cbvex2v  2341  cbvex  2399  cbvex2  2412  2ralorOLD  3230  rexcom  3288  cbvrexfw  3303  ceqsex  3522  ceqsexv  3524  gencbval  3536  ceqsralbv  3643  snnzb  4720  raldifsnb  4797  uni0b  4935  opab0  5552  tsna1  36949  ralopabb  42094