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 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  320  con4bii  321  con2bi  354  nbn2  371  pm5.32  574  norass  1535  hadnot  1604  had0  1606  cbvexdw  2336  cbvexd  2408  rexbiOLD  3174  vtoclgft  3492  rexprg  4632  isocnv3  7203  suppimacnv  7990  sumodd  16097  f1omvdco3  19057  ist0cld  31783  onsuct0  34630  bj-cbvexdv  34982  wl-3xornot  35652  ifpbi1  41084  ifpbi13  41096  abciffcbatnabciffncba  44424  abciffcbatnabciffncbai  44425  ichn  44908