Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > notbii | Unicode 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 661 | . 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 609 ax-in2 610 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sylnbi 673 xchnxbi 675 xchbinx 677 nndc 846 xorcom 1383 xordidc 1394 sbn 1945 neirr 2349 dfrex2dc 2461 ddifstab 3259 dfss4st 3360 ssddif 3361 difin 3364 difundi 3379 difindiss 3381 indifdir 3383 rabeq0 3443 abeq0 3444 snprc 3646 difprsnss 3716 uni0b 3819 disjnim 3978 brdif 4040 unidif0 4151 dtruex 4541 dcextest 4563 difopab 4742 cnvdif 5015 imadiflem 5275 imadif 5276 brprcneu 5487 poxp 6209 finexdc 6878 snexxph 6925 infmoti 7003 ismkvnex 7129 pw1nel3 7201 onntri35 7207 prltlu 7442 recexprlemdisj 7585 axpre-apti 7840 dfinfre 8865 fzdifsuc 10030 fzp1nel 10053 ntreq0 12891 bj-nnor 13734 bj-nndcALT 13758 nnti 13992 |
Copyright terms: Public domain | W3C validator |