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 299 | . 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-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpbiran 924 truan 1348 rexv 2704 reuv 2705 rmov 2706 rabab 2707 euxfrdc 2870 euind 2871 dfdif3 3186 ddifstab 3208 vss 3410 mptv 4025 regexmidlem1 4448 peano5 4512 intirr 4925 fvopab6 5517 riotav 5735 mpov 5861 brtpos0 6149 frec0g 6294 inl11 6950 apreim 8365 clim0 11054 gcd0id 11667 isbasis3g 12213 opnssneib 12325 ssidcn 12379 bj-d0clsepcl 13123 |
Copyright terms: Public domain | W3C validator |