![]() |
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 666 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: sylnbi 678 xchnxbi 680 xchbinx 682 nndc 851 xorcom 1388 xordidc 1399 sbn 1952 neirr 2356 dfrex2dc 2468 ddifstab 3269 dfss4st 3370 ssddif 3371 difin 3374 difundi 3389 difindiss 3391 indifdir 3393 rabeq0 3454 abeq0 3455 snprc 3659 difprsnss 3732 uni0b 3836 disjnim 3996 brdif 4058 unidif0 4169 dtruex 4560 dcextest 4582 difopab 4762 cnvdif 5037 imadiflem 5297 imadif 5298 brprcneu 5510 poxp 6235 finexdc 6904 snexxph 6951 infmoti 7029 ismkvnex 7155 pw1nel3 7232 onntri35 7238 netap 7255 prltlu 7488 recexprlemdisj 7631 axpre-apti 7886 dfinfre 8915 fzdifsuc 10083 fzp1nel 10106 ntreq0 13671 bj-nnor 14525 bj-nndcALT 14549 nnti 14783 |
Copyright terms: Public domain | W3C validator |