![]() |
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 226 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | imbi12i.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | imbi1i 238 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitri 184 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: stdcn 848 nfbii 1484 sbi2v 1904 sbim 1969 sb8mo 2056 cbvmo 2082 necon4ddc 2436 raleqbii 2506 rmo5 2714 cbvrmo 2725 ss2ab 3248 snsssn 3788 trint 4143 ssextss 4250 ordsoexmid 4595 zfregfr 4607 tfi 4615 peano2 4628 peano5 4631 relop 4813 dmcosseq 4934 cotr 5048 issref 5049 cnvsym 5050 intasym 5051 intirr 5053 codir 5055 qfto 5056 cnvpom 5209 cnvsom 5210 funcnvuni 5324 poxp 6287 infmoti 7089 dfinfre 8977 bezoutlembi 12145 algcvgblem 12190 isprm2 12258 ntreq0 14311 ss1oel2o 15554 |
Copyright terms: Public domain | W3C validator |