![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > bi2 | Unicode version |
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.) |
Ref | Expression |
---|---|
bi2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfbi1 192 | . 2 | |
2 | simprim 150 | . 2 | |
3 | 1, 2 | sylbi 195 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -. wn 3 -> wi 4
<-> wb 184 |
This theorem is referenced by: bicom1 199 pm5.74 244 bi3antOLD 289 bija 355 simplbi2comt 626 pm4.72 876 albi 1639 exbi 1666 cbv2h 2019 equveli 2088 equveliOLD 2089 euex 2308 2eu6 2383 2eu6OLD 2384 eleq2d 2527 ceqsalt 3132 euind 3286 reu6 3288 reuind 3303 sbciegft 3358 axpr 4690 iota4 5574 fv3 5884 nn0prpwlem 30140 nn0prpw 30141 tsbi3 30542 axc11next 31313 pm13.192 31317 exbir 33219 con5 33292 sbcim2g 33309 trsspwALT 33616 trsspwALT2 33617 sspwtr 33619 sspwtrALT 33620 pwtrVD 33624 pwtrrVD 33625 snssiALTVD 33627 sstrALT2VD 33634 sstrALT2 33635 suctrALT2VD 33636 eqsbc3rVD 33640 simplbi2VD 33646 exbirVD 33653 exbiriVD 33654 imbi12VD 33673 sbcim2gVD 33675 simplbi2comtVD 33688 con5VD 33700 2uasbanhVD 33711 bj-bi3ant 34178 bj-cbv2hv 34294 bj-ceqsalt0 34449 bj-ceqsalt1 34450 mapdrvallem2 37372 |
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 |
Copyright terms: Public domain | W3C validator |