con4bii - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > con4bii		Structured version Visualization version GIF version

Theorem con4bii 320

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

Colors of variables: wff setvar class

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 374 equsexvw 2000 cbvexv1 2332 cbvex2v 2334 cbvex 2392 cbvex2 2405 2ralorOLD 3220 rexcom 3278 cbvrexfw 3293 ceqsex 3514 ceqsexv 3516 gencbval 3528 ceqsralbv 3641 snnzb 4723 raldifsnb 4800 uni0b 4936 opab0 5555 tsna1 37687 ralopabb 42906

	
		OSZAR »