![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biimpr | Unicode version |
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.) |
Ref | Expression |
---|---|
biimpr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-bi 117 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simpli 111 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | simprd 114 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: bicom1 131 pm5.74 179 bi3ant 224 pm5.32d 450 notbi 666 nbn2 697 pm4.72 827 con4biddc 857 con1biimdc 873 bijadc 882 pclem6 1374 exbir 1436 simplbi2comg 1443 albi 1468 exbi 1604 equsexd 1729 cbv2h 1748 cbv2w 1750 sbiedh 1787 ceqsalt 2763 spcegft 2816 elab3gf 2887 euind 2924 reu6 2926 reuind 2942 sbciegft 2993 iota4 5196 fv3 5538 algcvgblem 12043 bj-inf2vnlem1 14604 |
Copyright terms: Public domain | W3C validator |