Theorem notbi 321

Description: Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. (Contributed by NM, 21-May-1994.) (Proof shortened by Wolf Lammen, 12-Jun-2013.)

Assertion

Ref	Expression
notbi	⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))

Proof of Theorem notbi

Step	Hyp	Ref	Expression
1		id 22	. . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 ↔ 𝜓))
2	1	notbid 320	. 2 ⊢ ((𝜑 ↔ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
3		id 22	. . 3 ⊢ ((¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
4	3	con4bid 319	. 2 ⊢ ((¬ 𝜑 ↔ ¬ 𝜓) → (𝜑 ↔ 𝜓))
5	2, 4	impbii 211	1 ⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  notbii  322  con4bii  323  con2bi  355  nbn2  372  nbbn  385  pm5.32  581  norass  1558  hadnot  1623  had0  1625  cbvexdw  2371  cbvexd  2440  rexprg  4657  isocnv3  7317  suppimacnv  8155  sumodd  16423  f1omvdco3  19490  ist0cld  34131  onsuct0  36802  bj-cbvexdv  37286  wl-3xornot  37976  ifpbi1  44054  ifpbi13  44066  abciffcbatnabciffncba  47524  abciffcbatnabciffncbai  47525  ichn  48063