![]() |
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 1965 sb8mo 2052 cbvmo 2078 necon4ddc 2432 raleqbii 2502 rmo5 2706 cbvrmo 2717 ss2ab 3238 snsssn 3776 trint 4131 ssextss 4238 ordsoexmid 4579 zfregfr 4591 tfi 4599 peano2 4612 peano5 4615 relop 4795 dmcosseq 4916 cotr 5028 issref 5029 cnvsym 5030 intasym 5031 intirr 5033 codir 5035 qfto 5036 cnvpom 5189 cnvsom 5190 funcnvuni 5304 poxp 6257 infmoti 7057 dfinfre 8943 bezoutlembi 12038 algcvgblem 12081 isprm2 12149 ntreq0 14089 ss1oel2o 15202 |
Copyright terms: Public domain | W3C validator |