![]() |
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 233 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | imbi12d.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | bibi2d 232 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitrd 188 |
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: pm5.32 453 bi2bian9 608 cleqh 2289 abbi 2303 cleqf 2357 cbvreuvw 2724 vtoclb 2809 vtoclbg 2813 ceqsexg 2880 elabgf 2894 reu6 2941 ru 2976 sbcbig 3024 sbcne12g 3090 sbcnestgf 3123 preq12bg 3788 nalset 4148 undifexmid 4208 exmidsssn 4217 exmidsssnc 4218 exmidundif 4221 opthg 4253 opelopabsb 4275 wetriext 4591 opeliunxp2 4782 resieq 4932 elimasng 5011 cbviota 5198 iota2df 5217 fnbrfvb 5572 fvelimab 5588 fmptco 5698 fsng 5705 fressnfv 5719 funfvima3 5766 isorel 5825 isocnv 5828 isocnv2 5829 isotr 5833 ovg 6030 caovcang 6053 caovordg 6059 caovord3d 6062 caovord 6063 opeliunxp2f 6257 dftpos4 6282 ecopovsym 6649 ecopovsymg 6652 xpf1o 6862 nneneq 6875 supmoti 7010 supsnti 7022 isotilem 7023 isoti 7024 ltanqg 7417 ltmnqg 7418 elinp 7491 prnmaxl 7505 prnminu 7506 ltasrg 7787 axpre-ltadd 7903 zextle 9362 zextlt 9363 xlesubadd 9901 rexfiuz 11016 climshft 11330 dvdsext 11879 ltoddhalfle 11916 halfleoddlt 11917 bezoutlemmo 12025 bezoutlemeu 12026 bezoutlemle 12027 bezoutlemsup 12028 dfgcd3 12029 dvdssq 12050 rpexp 12171 pcdvdsb 12337 isnsg 13107 nsgbi 13109 elnmz 13113 nmzbi 13114 nmznsg 13118 islidlm 13756 xmeteq0 14256 comet 14396 dedekindeulemuub 14492 dedekindeulemloc 14494 dedekindicclemuub 14501 dedekindicclemloc 14503 logltb 14692 bj-nalset 15044 bj-d0clsepcl 15074 bj-nn0sucALT 15127 ltlenmkv 15216 |
Copyright terms: Public domain | W3C validator |