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 3444 abeq0 3445 snprc 3648 difprsnss 3718 uni0b 3821 disjnim 3980 brdif 4042 unidif0 4153 dtruex 4543 dcextest 4565 difopab 4744 cnvdif 5017 imadiflem 5277 imadif 5278 brprcneu 5489 poxp 6211 finexdc 6880 snexxph 6927 infmoti 7005 ismkvnex 7131 pw1nel3 7208 onntri35 7214 prltlu 7449 recexprlemdisj 7592 axpre-apti 7847 dfinfre 8872 fzdifsuc 10037 fzp1nel 10060 ntreq0 12926 bj-nnor 13769 bj-nndcALT 13793 nnti 14027 |
Copyright terms: Public domain | W3C validator |