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 438 3anibar 1150 drex1 1778 elrab3t 2867 bnd2 4137 opbrop 4668 opelresi 4880 funcnv3 5235 fnssresb 5285 dff1o5 5426 fneqeql2 5579 fnniniseg2 5593 rexsupp 5594 dffo3 5617 fmptco 5636 fnressn 5656 fconst4m 5690 riota2df 5803 eloprabga 5911 frecabcl 6349 mptelixpg 6682 exmidfodomrlemreseldju 7138 enq0breq 7359 genpassl 7447 genpassu 7448 elnnnn0 9139 peano2z 9209 znnsub 9224 znn0sub 9238 uzin 9477 nn01to3 9533 rpnegap 9600 negelrp 9601 xsubge0 9792 divelunit 9913 elfz5 9927 uzsplit 10001 elfzonelfzo 10139 adddivflid 10201 divfl0 10205 2shfti 10743 rexuz3 10902 clim2c 11193 fisumss 11301 infssuzex 11849 bezoutlemmain 11898 eltg3 12553 lmbrf 12711 cnrest2 12732 cnptoprest 12735 cnptoprest2 12736 ismet2 12850 elbl2ps 12888 elbl2 12889 xblpnfps 12894 xblpnf 12895 bdxmet 12997 metcn 13010 cnbl0 13030 cnblcld 13031 mulc1cncf 13072 ellimc3apf 13125 pilem1 13196 |
Copyright terms: Public domain | W3C validator |