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: wa 103 wb 104 |
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 386 mpbiran2 925 isset 2692 rexcom4b 2711 eueq 2855 ssrabeq 3183 a9evsep 4050 pwunim 4208 elvv 4601 elvvv 4602 resopab 4863 funfn 5153 dffn2 5274 dffn3 5283 dffn4 5351 fsn 5592 ixp0x 6620 ac6sfi 6792 fimax2gtri 6795 xrmaxiflemcom 11018 |
Copyright terms: Public domain | W3C validator |