Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > notbii | GIF version |
Description: Equivalence property for negation. Inference form. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
notbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
notbii | ⊢ (¬ 𝜑 ↔ ¬ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notbii.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
2 | notbi 640 | . 2 ⊢ ((𝜑 ↔ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (¬ 𝜑 ↔ ¬ 𝜓) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 588 ax-in2 589 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sylnbi 652 xchnxbi 654 xchbinx 656 nndc 821 xorcom 1351 xordidc 1362 sbn 1903 neirr 2294 dfrex2dc 2405 ddifstab 3178 dfss4st 3279 ssddif 3280 difin 3283 difundi 3298 difindiss 3300 indifdir 3302 rabeq0 3362 abeq0 3363 snprc 3558 difprsnss 3628 uni0b 3731 disjnim 3890 brdif 3951 unidif0 4061 dtruex 4444 dcextest 4465 difopab 4642 cnvdif 4915 imadiflem 5172 imadif 5173 brprcneu 5382 poxp 6097 finexdc 6764 snexxph 6806 infmoti 6883 ismkvnex 6997 prltlu 7263 recexprlemdisj 7406 axpre-apti 7661 dfinfre 8682 fzdifsuc 9829 fzp1nel 9852 ntreq0 12228 bj-nnor 12873 bj-nndcALT 12890 nnti 13118 |
Copyright terms: Public domain | W3C validator |