![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bibi12d | Unicode version |
Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imbi12d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
imbi12d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bibi12d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi12d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | bibi1d 222 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | imbi12d.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | bibi2d 221 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitrd 177 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm5.32 426 bi2bian9 540 cleqh 2134 abbi 2148 cleqf 2198 vtoclb 2605 vtoclbg 2608 ceqsexg 2666 elabgf 2679 reu6 2724 ru 2757 sbcbig 2803 sbcne12g 2862 sbcnestgf 2891 preq12bg 3535 nalset 3878 opthg 3966 opelopabsb 3988 opeliunxp2 4419 resieq 4565 elimasng 4636 cbviota 4815 iota2df 4834 fnbrfvb 5157 fvelimab 5172 fmptco 5273 fsng 5279 fressnfv 5293 funfvima3 5335 isorel 5391 isocnv 5394 isocnv2 5395 isotr 5399 ovg 5581 caovcang 5604 caovordg 5610 caovord3d 5613 caovord 5614 dftpos4 5819 ecopovsym 6138 ecopovsymg 6141 ltanqg 6384 ltmnqg 6385 elinp 6457 prnmaxl 6471 prnminu 6472 ltasrg 6698 axpre-ltadd 6770 zextle 8107 zextlt 8108 bj-nalset 9350 bj-d0clsepcl 9384 bj-nn0sucALT 9438 |
Copyright terms: Public domain | W3C validator |