New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > bibi12i | Unicode version |
Description: The equivalence of two equivalences. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bibi.a | |
bibi12.2 |
Ref | Expression |
---|---|
bibi12i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bibi12.2 | . . 3 | |
2 | 1 | bibi2i 304 | . 2 |
3 | bibi.a | . . 3 | |
4 | 3 | bibi1i 305 | . 2 |
5 | 2, 4 | bitri 240 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 |
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 177 |
This theorem is referenced by: pm5.32 617 orbidi 898 pm5.7 900 xorbi12i 1314 axcnvprim 4091 axsiprim 4093 axins2prim 4095 axins3prim 4096 pw111 4170 cnvkexg 4286 ssetkex 4294 sikexg 4296 ins2kexg 4305 ins3kexg 4306 dfaddc2 4381 nnsucelrlem1 4424 ltfinex 4464 eqpwrelk 4478 eqpw1relk 4479 eqtfinrelk 4486 evenfinex 4503 oddfinex 4504 evenodddisjlem1 4515 nnadjoinlem1 4519 srelk 4524 tfinnnlem1 4533 dfop2lem1 4573 setconslem2 4732 setconslem3 4733 setconslem7 4737 dfswap2 4741 isocnv2 5492 brimage 5793 releqel 5807 releqmpt2 5809 extex 5915 qsexg 5982 ovcelem1 6171 tcfnex 6244 |
Copyright terms: Public domain | W3C validator |