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 843 con1biimdc 859 bijadc 868 pclem6 1356 albi 1448 exbi 1584 equsexd 1709 cbv2h 1728 cbv2w 1730 sbiedh 1767 eumo0 2037 ceqsalt 2738 vtoclgft 2762 spcgft 2789 pm13.183 2850 reu6 2901 reu3 2902 sbciegft 2967 ddifstab 3239 exmidsssnc 4164 fv3 5490 prnmaxl 7402 prnminu 7403 elabgft1 13323 elabgf2 13325 bj-axemptylem 13438 bj-inf2vn 13520 bj-inf2vn2 13521 bj-nn0sucALT 13524 |
Copyright terms: Public domain | W3C validator |