![]() |
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 284 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 7 |
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 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm4.71 369 mpbiran2 847 isset 2555 rexcom4b 2573 eueq 2706 ssrabeq 3020 nsspssun 3164 disjpss 3272 a9evsep 3870 pwunim 4014 elvv 4345 elvvv 4346 resopab 4595 funfn 4874 dffn2 4990 dffn3 4996 dffn4 5055 fsn 5278 |
Copyright terms: Public domain | W3C validator |