![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biantrurd | Unicode version |
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
biantrud.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
biantrurd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biantrud.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ibar 285 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
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-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3anibar 1071 drex1 1676 elrab3t 2691 bnd2 3917 opbrop 4362 opelresi 4566 funcnv3 4904 fnssresb 4954 dff1o5 5078 fneqeql2 5219 fnniniseg2 5233 rexsupp 5234 dffo3 5257 fmptco 5273 fnressn 5292 fconst4m 5324 riota2df 5431 eloprabga 5533 enq0breq 6419 genpassl 6507 genpassu 6508 elnnnn0 8001 peano2z 8057 znnsub 8072 znn0sub 8085 uzin 8281 nn01to3 8328 rpnegap 8390 divelunit 8640 elfz5 8652 uzsplit 8724 elfzonelfzo 8856 |
Copyright terms: Public domain | W3C validator |