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 285 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3anibar 1072 drex1 1679 elrab3t 2697 bnd2 3926 opbrop 4419 opelresi 4623 funcnv3 4961 fnssresb 5011 dff1o5 5135 fneqeql2 5276 fnniniseg2 5290 rexsupp 5291 dffo3 5314 fmptco 5330 fnressn 5349 fconst4m 5381 riota2df 5488 eloprabga 5591 enq0breq 6534 genpassl 6622 genpassu 6623 elnnnn0 8225 peano2z 8281 znnsub 8296 znn0sub 8309 uzin 8505 nn01to3 8552 rpnegap 8615 divelunit 8870 elfz5 8882 uzsplit 8954 elfzonelfzo 9086 adddivflid 9134 divfl0 9138 2shfti 9432 rexuz3 9588 clim2c 9805 |
Copyright terms: Public domain | W3C validator |