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: wa 97 wb 98 |
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 848 isset 2561 rexcom4b 2579 eueq 2712 ssrabeq 3026 nsspssun 3170 disjpss 3278 a9evsep 3879 pwunim 4023 elvv 4402 elvvv 4403 resopab 4652 funfn 4931 dffn2 5047 dffn3 5053 dffn4 5112 fsn 5335 ac6sfi 6352 |
Copyright terms: Public domain | W3C validator |