Theorem notbi 319

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 318	. 2 ⊢ ((𝜑 ↔ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
3		id 22	. . 3 ⊢ ((¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
4	3	con4bid 317	. 2 ⊢ ((¬ 𝜑 ↔ ¬ 𝜓) → (𝜑 ↔ 𝜓))
5	2, 4	impbii 209	1 ⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  notbii  320  con4bii  321  con2bi  353  nbn2  370  pm5.32  573  norass  1534  hadnot  1599  had0  1601  cbvexdw  2340  cbvexd  2411  rexbiOLD  3103  rexprg  4702  isocnv3  7352  suppimacnv  8198  sumodd  16422  f1omvdco3  19482  ist0cld  33794  onsuct0  36424  bj-cbvexdv  36783  wl-3xornot  37464  ifpbi1  43467  ifpbi13  43479  abciffcbatnabciffncba  46879  abciffcbatnabciffncbai  46880  ichn  47381