![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > bi1 | Structured version Unicode version |
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) |
Ref | Expression |
---|---|
bi1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-bi 185 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | simplim 151 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | simplim 151 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | syl 16 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 185 |
This theorem is referenced by: biimpi 194 bicom1 199 biimpd 207 ibd 243 pm5.74 244 bi3antOLD 289 pm5.501 341 bija 355 bianir 958 albi 1610 exbi 1634 cbv2h 1978 equveliOLD 2049 sbiedOLD 2113 mo2v 2269 mo2vOLD 2270 mo2vOLDOLD 2271 eumo0OLD 2300 2eu6 2380 2eu6OLD 2381 eleq2d 2524 ceqsalt 3101 vtoclgft 3126 spcgft 3155 pm13.183 3207 reu6 3255 reu3 3256 sbciegft 3325 fv3 5815 expeq0 12015 t1t0 19094 kqfvima 19445 ufileu 19634 cvmlift2lem1 27358 btwndiff 28225 nn0prpw 28689 bi33imp12 31549 bi23imp1 31554 bi123imp0 31555 eqsbc3rVD 31931 imbi12VD 31964 2uasbanhVD 32002 bj-dfbi6 32434 bj-bi3ant 32470 bj-cbv2hv 32587 bj-eumo0 32706 bj-ceqsalt0 32741 bj-ceqsalt1 32742 bj-ax9 32756 |
Copyright terms: Public domain | W3C validator |