![]() |
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 300 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
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 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: mpbiran2d 442 posng 4698 elrnmpt1 4878 fliftf 5799 elxp7 6170 eroveu 6625 sbthlemi5 6959 sbthlemi6 6960 elfi2 6970 reapltxor 8545 divap0b 8639 nnle1eq1 8942 nn0le0eq0 9203 nn0lt10b 9332 ioopos 9949 xrmaxiflemcom 11256 fz1f1o 11382 nndivdvds 11802 dvdsmultr2 11839 pcmpt 12340 pcmpt2 12341 discld 13606 cncnpi 13698 cnptoprest2 13710 lmss 13716 txcn 13745 isxmet2d 13818 xblss2 13875 bdxmet 13971 xmetxp 13977 cncfcdm 14039 lgsneg 14395 lgsdilem 14398 |
Copyright terms: Public domain | W3C validator |