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 817 nfbii 1434 sbi2v 1848 sbim 1904 sb8mo 1991 cbvmo 2017 necon4ddc 2357 raleqbii 2424 rmo5 2623 cbvrmo 2630 ss2ab 3135 snsssn 3658 trint 4011 ssextss 4112 ordsoexmid 4447 zfregfr 4458 tfi 4466 peano2 4479 peano5 4482 relop 4659 dmcosseq 4780 cotr 4890 issref 4891 cnvsym 4892 intasym 4893 intirr 4895 codir 4897 qfto 4898 cnvpom 5051 cnvsom 5052 funcnvuni 5162 poxp 6097 infmoti 6883 dfinfre 8682 bezoutlembi 11620 algcvgblem 11657 isprm2 11725 ntreq0 12228 ss1oel2o 13116 |
Copyright terms: Public domain | W3C validator |