Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE 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 215 | . 2 |
3 | imbi12i.1 | . . 3 | |
4 | 3 | imbi1i 227 | . 2 |
5 | 2, 4 | bitri 173 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: nfbii 1362 sbi2v 1772 sbim 1827 sb8mo 1914 cbvmo 1940 necon4ddc 2277 raleqbii 2336 rmo5 2525 cbvrmo 2532 ss2ab 3008 snsssn 3532 trint 3869 ssextss 3956 ordsoexmid 4286 zfregfr 4298 tfi 4305 peano2 4318 peano5 4321 relop 4486 dmcosseq 4603 cotr 4706 issref 4707 cnvsym 4708 intasym 4709 intirr 4711 codir 4713 qfto 4714 cnvpom 4860 cnvsom 4861 funcnvuni 4968 poxp 5853 algcvgblem 9888 peano5setOLD 10065 |
Copyright terms: Public domain | W3C validator |