![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biantrud | Unicode version |
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.) |
Ref | Expression |
---|---|
biantrud.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
biantrud |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biantrud.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | iba 296 |
. 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-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpbiran2d 436 posng 4571 elrnmpt1 4750 fliftf 5654 elxp7 6022 eroveu 6474 sbthlemi5 6801 sbthlemi6 6802 elfi2 6812 reapltxor 8266 divap0b 8353 nnle1eq1 8651 nn0le0eq0 8906 nn0lt10b 9032 ioopos 9623 xrmaxiflemcom 10907 fz1f1o 11033 nndivdvds 11344 dvdsmultr2 11378 discld 12145 cncnpi 12236 cnptoprest2 12248 lmss 12254 txcn 12283 isxmet2d 12334 xblss2 12391 bdxmet 12487 xmetxp 12493 cncffvrn 12552 |
Copyright terms: Public domain | W3C validator |