![]() |
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 4700 elrnmpt1 4880 fliftf 5802 elxp7 6173 eroveu 6628 sbthlemi5 6962 sbthlemi6 6963 elfi2 6973 reapltxor 8548 divap0b 8642 nnle1eq1 8945 nn0le0eq0 9206 nn0lt10b 9335 ioopos 9952 xrmaxiflemcom 11259 fz1f1o 11385 nndivdvds 11805 dvdsmultr2 11842 pcmpt 12343 pcmpt2 12344 lssle0 13463 discld 13675 cncnpi 13767 cnptoprest2 13779 lmss 13785 txcn 13814 isxmet2d 13887 xblss2 13944 bdxmet 14040 xmetxp 14046 cncfcdm 14108 lgsneg 14464 lgsdilem 14467 |
Copyright terms: Public domain | W3C validator |