![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biantru | Unicode version |
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
biantru.1 |
![]() ![]() |
Ref | Expression |
---|---|
biantru |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biantru.1 |
. 2
![]() ![]() | |
2 | iba 298 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm4.71 387 mpbiran2 926 isset 2695 rexcom4b 2714 eueq 2859 ssrabeq 3188 a9evsep 4058 pwunim 4216 elvv 4609 elvvv 4610 resopab 4871 funfn 5161 dffn2 5282 dffn3 5291 dffn4 5359 fsn 5600 ixp0x 6628 ac6sfi 6800 fimax2gtri 6803 xrmaxiflemcom 11050 trirec0xor 13413 |
Copyright terms: Public domain | W3C validator |