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  352  nbn2  369  pm5.32  572  norass  1531  hadnot  1596  had0  1598  cbvexdw  2330  cbvexd  2402  rexbiOLD  3095  rexprg  4705  isocnv3  7344  suppimacnv  8188  sumodd  16390  f1omvdco3  19447  ist0cld  33635  onsuct0  36136  bj-cbvexdv  36488  wl-3xornot  37171  ifpbi1  43127  ifpbi13  43139  abciffcbatnabciffncba  46527  abciffcbatnabciffncbai  46528  ichn  47011

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »