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 655 | . 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 603 ax-in2 604 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sylnbi 667 xchnxbi 669 xchbinx 671 nndc 836 xorcom 1366 xordidc 1377 sbn 1925 neirr 2317 dfrex2dc 2428 ddifstab 3208 dfss4st 3309 ssddif 3310 difin 3313 difundi 3328 difindiss 3330 indifdir 3332 rabeq0 3392 abeq0 3393 snprc 3588 difprsnss 3658 uni0b 3761 disjnim 3920 brdif 3981 unidif0 4091 dtruex 4474 dcextest 4495 difopab 4672 cnvdif 4945 imadiflem 5202 imadif 5203 brprcneu 5414 poxp 6129 finexdc 6796 snexxph 6838 infmoti 6915 ismkvnex 7029 prltlu 7295 recexprlemdisj 7438 axpre-apti 7693 dfinfre 8714 fzdifsuc 9861 fzp1nel 9884 ntreq0 12301 bj-nnor 12946 bj-nndcALT 12963 nnti 13191 |
Copyright terms: Public domain | W3C validator |