Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biantrurd | Unicode version |
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
biantrud.1 |
Ref | Expression |
---|---|
biantrurd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biantrud.1 | . 2 | |
2 | ibar 299 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 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: mpbirand 437 3anibar 1134 drex1 1754 elrab3t 2812 bnd2 4067 opbrop 4588 opelresi 4800 funcnv3 5155 fnssresb 5205 dff1o5 5344 fneqeql2 5497 fnniniseg2 5511 rexsupp 5512 dffo3 5535 fmptco 5554 fnressn 5574 fconst4m 5608 riota2df 5718 eloprabga 5826 frecabcl 6264 mptelixpg 6596 exmidfodomrlemreseldju 7024 enq0breq 7212 genpassl 7300 genpassu 7301 elnnnn0 8988 peano2z 9058 znnsub 9073 znn0sub 9087 uzin 9326 nn01to3 9377 rpnegap 9442 negelrp 9443 xsubge0 9632 divelunit 9753 elfz5 9766 uzsplit 9840 elfzonelfzo 9975 adddivflid 10033 divfl0 10037 2shfti 10571 rexuz3 10730 clim2c 11021 fisumss 11129 infssuzex 11569 bezoutlemmain 11613 eltg3 12153 lmbrf 12311 cnrest2 12332 cnptoprest 12335 cnptoprest2 12336 ismet2 12450 elbl2ps 12488 elbl2 12489 xblpnfps 12494 xblpnf 12495 bdxmet 12597 metcn 12610 cnbl0 12630 cnblcld 12631 mulc1cncf 12672 ellimc3apf 12725 pilem1 12787 |
Copyright terms: Public domain | W3C validator |