New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > imbi12i | Unicode version |
Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imbi12i.1 | |
imbi12i.2 |
Ref | Expression |
---|---|
imbi12i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi12i.2 | . . 3 | |
2 | 1 | imbi2i 303 | . 2 |
3 | imbi12i.1 | . . 3 | |
4 | 3 | imbi1i 315 | . 2 |
5 | 2, 4 | bitri 240 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: orimdi 820 rb-bijust 1514 nfbii 1569 sb8mo 2223 cbvmo 2241 raleqbii 2644 rmo5 2827 cbvrmo 2834 ss2ab 3334 sscon34 3661 evenodddisjlem1 4515 tfinnn 4534 cotr 5026 cnvsym 5027 intasym 5028 intirr 5029 dffun2 5119 funcnvuni 5161 fvfullfunlem1 5861 clos1induct 5880 |
Copyright terms: Public domain | W3C validator |