![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biantrur | Unicode version |
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
biantrur.1 |
![]() ![]() |
Ref | Expression |
---|---|
biantrur |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biantrur.1 |
. 2
![]() ![]() | |
2 | ibar 295 |
. 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-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: mpbiran 882 truan 1302 rexv 2628 reuv 2629 rmov 2630 rabab 2631 euxfrdc 2789 euind 2790 dfdif3 3094 ddifstab 3116 vss 3312 mptv 3900 regexmidlem1 4312 peano5 4376 intirr 4773 fvopab6 5341 riotav 5552 mpt2v 5673 brtpos0 5949 frec0g 6094 apreim 7980 clim0 10498 gcd0id 10750 bj-d0clsepcl 11163 |
Copyright terms: Public domain | W3C validator |