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 225 | . 2 |
3 | imbi12i.1 | . . 3 | |
4 | 3 | imbi1i 237 | . 2 |
5 | 2, 4 | bitri 183 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: stdcn 842 nfbii 1466 sbi2v 1885 sbim 1946 sb8mo 2033 cbvmo 2059 necon4ddc 2412 raleqbii 2482 rmo5 2685 cbvrmo 2695 ss2ab 3215 snsssn 3748 trint 4102 ssextss 4205 ordsoexmid 4546 zfregfr 4558 tfi 4566 peano2 4579 peano5 4582 relop 4761 dmcosseq 4882 cotr 4992 issref 4993 cnvsym 4994 intasym 4995 intirr 4997 codir 4999 qfto 5000 cnvpom 5153 cnvsom 5154 funcnvuni 5267 poxp 6211 infmoti 7005 dfinfre 8872 bezoutlembi 11960 algcvgblem 12003 isprm2 12071 ntreq0 12926 ss1oel2o 14026 |
Copyright terms: Public domain | W3C validator |