![]() |
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 296 |
. 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 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpbiran 887 truan 1307 rexv 2638 reuv 2639 rmov 2640 rabab 2641 euxfrdc 2802 euind 2803 dfdif3 3111 ddifstab 3133 vss 3334 mptv 3941 regexmidlem1 4362 peano5 4426 intirr 4831 fvopab6 5410 riotav 5627 mpt2v 5752 brtpos0 6031 frec0g 6176 apreim 8134 clim0 10727 gcd0id 11302 isbasis3g 11798 bj-d0clsepcl 12086 |
Copyright terms: Public domain | W3C validator |