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 833 nfbii 1453 sbi2v 1872 sbim 1933 sb8mo 2020 cbvmo 2046 necon4ddc 2399 raleqbii 2469 rmo5 2672 cbvrmo 2679 ss2ab 3196 snsssn 3724 trint 4077 ssextss 4180 ordsoexmid 4521 zfregfr 4533 tfi 4541 peano2 4554 peano5 4557 relop 4736 dmcosseq 4857 cotr 4967 issref 4968 cnvsym 4969 intasym 4970 intirr 4972 codir 4974 qfto 4975 cnvpom 5128 cnvsom 5129 funcnvuni 5239 poxp 6179 infmoti 6972 dfinfre 8827 bezoutlembi 11888 algcvgblem 11925 isprm2 11993 ntreq0 12532 ss1oel2o 13565 |
Copyright terms: Public domain | W3C validator |