![]() |
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 301 |
. 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-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: mpbiran 940 truan 1370 rexv 2755 reuv 2756 rmov 2757 rabab 2758 euxfrdc 2923 euind 2924 dfdif3 3245 ddifstab 3267 vss 3470 mptv 4097 regexmidlem1 4528 peano5 4593 intirr 5010 fvopab6 5607 riotav 5829 mpov 5958 brtpos0 6246 frec0g 6391 inl11 7057 apreim 8537 clim0 11264 gcd0id 11950 nnwosdc 12010 isbasis3g 13177 opnssneib 13289 ssidcn 13343 bj-d0clsepcl 14299 |
Copyright terms: Public domain | W3C validator |