Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biimp | Unicode version |
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
biimp |
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 446 notbi 656 pm5.19 696 con4biddc 847 con1biimdc 863 bijadc 872 pclem6 1364 albi 1456 exbi 1592 equsexd 1717 cbv2h 1736 cbv2w 1738 sbiedh 1775 eumo0 2045 ceqsalt 2752 vtoclgft 2776 spcgft 2803 pm13.183 2864 reu6 2915 reu3 2916 sbciegft 2981 ddifstab 3254 exmidsssnc 4182 fv3 5509 prnmaxl 7429 prnminu 7430 elabgft1 13659 elabgf2 13661 bj-axemptylem 13774 bj-inf2vn 13856 bj-inf2vn2 13857 bj-nn0sucALT 13860 |
Copyright terms: Public domain | W3C validator |