![]() |
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: ![]() ![]() ![]() |
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 1771 elrab3t 2843 bnd2 4105 opbrop 4626 opelresi 4838 funcnv3 5193 fnssresb 5243 dff1o5 5384 fneqeql2 5537 fnniniseg2 5551 rexsupp 5552 dffo3 5575 fmptco 5594 fnressn 5614 fconst4m 5648 riota2df 5758 eloprabga 5866 frecabcl 6304 mptelixpg 6636 exmidfodomrlemreseldju 7073 enq0breq 7268 genpassl 7356 genpassu 7357 elnnnn0 9044 peano2z 9114 znnsub 9129 znn0sub 9143 uzin 9382 nn01to3 9436 rpnegap 9503 negelrp 9504 xsubge0 9694 divelunit 9815 elfz5 9829 uzsplit 9903 elfzonelfzo 10038 adddivflid 10096 divfl0 10100 2shfti 10635 rexuz3 10794 clim2c 11085 fisumss 11193 infssuzex 11678 bezoutlemmain 11722 eltg3 12265 lmbrf 12423 cnrest2 12444 cnptoprest 12447 cnptoprest2 12448 ismet2 12562 elbl2ps 12600 elbl2 12601 xblpnfps 12606 xblpnf 12607 bdxmet 12709 metcn 12722 cnbl0 12742 cnblcld 12743 mulc1cncf 12784 ellimc3apf 12837 pilem1 12908 |
Copyright terms: Public domain | W3C validator |