![]() |
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 232 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | imbi12d.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | bibi2d 231 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitrd 187 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.32 442 bi2bian9 576 cleqh 2194 abbi 2208 cleqf 2259 vtoclb 2690 vtoclbg 2694 ceqsexg 2759 elabgf 2772 reu6 2818 ru 2853 sbcbig 2899 sbcne12g 2963 sbcnestgf 2993 preq12bg 3639 nalset 3990 undifexmid 4049 exmidsssn 4055 exmidundif 4058 opthg 4089 opelopabsb 4111 wetriext 4420 opeliunxp2 4607 resieq 4755 elimasng 4833 cbviota 5019 iota2df 5038 fnbrfvb 5380 fvelimab 5395 fmptco 5503 fsng 5509 fressnfv 5523 funfvima3 5567 isorel 5625 isocnv 5628 isocnv2 5629 isotr 5633 ovg 5821 caovcang 5844 caovordg 5850 caovord3d 5853 caovord 5854 opeliunxp2f 6041 dftpos4 6066 ecopovsym 6428 ecopovsymg 6431 xpf1o 6640 nneneq 6653 supmoti 6768 supsnti 6780 isotilem 6781 isoti 6782 ltanqg 7056 ltmnqg 7057 elinp 7130 prnmaxl 7144 prnminu 7145 ltasrg 7413 axpre-ltadd 7518 zextle 8936 zextlt 8937 xlesubadd 9449 rexfiuz 10537 climshft 10847 dvdsext 11283 ltoddhalfle 11320 halfleoddlt 11321 bezoutlemmo 11422 bezoutlemeu 11423 bezoutlemle 11424 bezoutlemsup 11425 dfgcd3 11426 dvdssq 11447 rpexp 11559 xmeteq0 12145 comet 12285 bj-nalset 12494 bj-d0clsepcl 12528 bj-nn0sucALT 12581 |
Copyright terms: Public domain | W3C validator |