Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bi1 | Unicode version |
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
bi1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-bi 116 | . . 3 | |
2 | 1 | simpli 110 | . 2 |
3 | 2 | simpld 111 | 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 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biimpi 119 bicom1 130 biimpd 143 ibd 177 pm5.74 178 bi3ant 223 pm5.501 243 pm5.32d 445 notbi 640 pm5.19 680 con4biddc 827 con1biimdc 843 bijadc 852 pclem6 1337 albi 1429 exbi 1568 equsexd 1692 cbv2h 1709 sbiedh 1745 eumo0 2008 ceqsalt 2686 vtoclgft 2710 spcgft 2737 pm13.183 2796 reu6 2846 reu3 2847 sbciegft 2911 ddifstab 3178 exmidsssnc 4096 fv3 5412 prnmaxl 7264 prnminu 7265 elabgft1 12912 elabgf2 12914 bj-axemptylem 13017 bj-inf2vn 13099 bj-inf2vn2 13100 bj-nn0sucALT 13103 |
Copyright terms: Public domain | W3C validator |