![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > notbii | Unicode version |
Description: Negate both sides of a logical equivalence. (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 | id 19 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | notbid 633 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | ax-mp 7 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sylnbi 644 xchnxbi 646 xchbinx 648 dcbii 791 xorcom 1334 xordidc 1345 sbn 1886 neirr 2276 dfrex2dc 2387 ddifstab 3155 dfss4st 3256 ssddif 3257 difin 3260 difundi 3275 difindiss 3277 indifdir 3279 rabeq0 3339 abeq0 3340 snprc 3535 difprsnss 3605 uni0b 3708 disjnim 3866 brdif 3923 unidif0 4031 dtruex 4412 dcextest 4433 difopab 4610 cnvdif 4881 imadiflem 5138 imadif 5139 brprcneu 5346 poxp 6059 finexdc 6725 snexxph 6766 infmoti 6830 prltlu 7196 recexprlemdisj 7339 axpre-apti 7570 dfinfre 8572 fzdifsuc 9702 fzp1nel 9725 ntreq0 12083 nndc 12549 nnti 12776 |
Copyright terms: Public domain | W3C validator |