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: 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: pm5.32 448 bi2bian9 597 cleqh 2237 abbi 2251 cleqf 2303 vtoclb 2738 vtoclbg 2742 ceqsexg 2808 elabgf 2821 reu6 2868 ru 2903 sbcbig 2950 sbcne12g 3015 sbcnestgf 3046 preq12bg 3695 nalset 4053 undifexmid 4112 exmidsssn 4120 exmidsssnc 4121 exmidundif 4124 opthg 4155 opelopabsb 4177 wetriext 4486 opeliunxp2 4674 resieq 4824 elimasng 4902 cbviota 5088 iota2df 5107 fnbrfvb 5455 fvelimab 5470 fmptco 5579 fsng 5586 fressnfv 5600 funfvima3 5644 isorel 5702 isocnv 5705 isocnv2 5706 isotr 5710 ovg 5902 caovcang 5925 caovordg 5931 caovord3d 5934 caovord 5935 opeliunxp2f 6128 dftpos4 6153 ecopovsym 6518 ecopovsymg 6521 xpf1o 6731 nneneq 6744 supmoti 6873 supsnti 6885 isotilem 6886 isoti 6887 ltanqg 7201 ltmnqg 7202 elinp 7275 prnmaxl 7289 prnminu 7290 ltasrg 7571 axpre-ltadd 7687 zextle 9135 zextlt 9136 xlesubadd 9659 rexfiuz 10754 climshft 11066 dvdsext 11542 ltoddhalfle 11579 halfleoddlt 11580 bezoutlemmo 11683 bezoutlemeu 11684 bezoutlemle 11685 bezoutlemsup 11686 dfgcd3 11687 dvdssq 11708 rpexp 11820 xmeteq0 12517 comet 12657 dedekindeulemuub 12753 dedekindeulemloc 12755 dedekindicclemuub 12762 dedekindicclemloc 12764 bj-nalset 13082 bj-d0clsepcl 13112 bj-nn0sucALT 13165 |
Copyright terms: Public domain | W3C validator |