Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biantrud | Unicode version |
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.) |
Ref | Expression |
---|---|
biantrud.1 |
Ref | Expression |
---|---|
biantrud |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biantrud.1 | . 2 | |
2 | iba 298 | . 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-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpbiran2d 439 posng 4670 elrnmpt1 4849 fliftf 5761 elxp7 6130 eroveu 6583 sbthlemi5 6917 sbthlemi6 6918 elfi2 6928 reapltxor 8478 divap0b 8570 nnle1eq1 8872 nn0le0eq0 9133 nn0lt10b 9262 ioopos 9877 xrmaxiflemcom 11176 fz1f1o 11302 nndivdvds 11722 dvdsmultr2 11758 pcmpt 12252 pcmpt2 12253 discld 12683 cncnpi 12775 cnptoprest2 12787 lmss 12793 txcn 12822 isxmet2d 12895 xblss2 12952 bdxmet 13048 xmetxp 13054 cncffvrn 13116 |
Copyright terms: Public domain | W3C validator |