Theorem notbi 318

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 317	. 2 ⊢ ((𝜑 ↔ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
3		id 22	. . 3 ⊢ ((¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
4	3	con4bid 316	. 2 ⊢ ((¬ 𝜑 ↔ ¬ 𝜓) → (𝜑 ↔ 𝜓))
5	2, 4	impbii 208	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:  notbii  319  con4bii  320  con2bi  353  nbn2  370  pm5.32  573  norass  1535  hadnot  1605  had0  1607  cbvexdw  2338  cbvexd  2408  rexbiOLD  3170  vtoclgft  3482  rexprg  4629  isocnv3  7183  suppimacnv  7961  sumodd  16025  f1omvdco3  18972  ist0cld  31685  onsuct0  34557  bj-cbvexdv  34909  wl-3xornot  35579  ifpbi1  40982  ifpbi13  40994  abciffcbatnabciffncba  44311  abciffcbatnabciffncbai  44312  ichn  44796