![]() |
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 4716 elrnmpt1 4896 fliftf 5821 elxp7 6196 eroveu 6653 sbthlemi5 6991 sbthlemi6 6992 elfi2 7002 reapltxor 8577 divap0b 8671 nnle1eq1 8974 nn0le0eq0 9235 nn0lt10b 9364 ioopos 9982 xrmaxiflemcom 11292 fz1f1o 11418 nndivdvds 11838 dvdsmultr2 11875 pcmpt 12378 pcmpt2 12379 lssle0 13705 discld 14113 cncnpi 14205 cnptoprest2 14217 lmss 14223 txcn 14252 isxmet2d 14325 xblss2 14382 bdxmet 14478 xmetxp 14484 cncfcdm 14546 lgsneg 14903 lgsdilem 14906 |
Copyright terms: Public domain | W3C validator |