![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anbi12i | Unicode version |
Description: Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
anbi12.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
anbi12.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
anbi12i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anbi12.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anbi1i 446 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | anbi12.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | anbi2i 445 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitri 182 |
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 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: anbi12ci 449 ordir 764 orddi 767 dcan 876 3anbi123i 1128 an6 1253 xorcom 1320 trubifal 1348 truxortru 1351 truxorfal 1352 falxortru 1353 falxorfal 1354 nford 1500 nfand 1501 sbequ8 1770 sbanv 1812 sban 1872 sbbi 1876 sbnf2 1900 eu1 1968 2exeu 2035 2eu4 2036 sbabel 2248 neanior 2336 rexeqbii 2385 r19.26m 2494 reean 2528 reu5 2572 reu2 2791 reu3 2793 eqss 3025 unss 3158 ralunb 3165 ssin 3206 undi 3230 difundi 3234 indifdir 3238 inab 3250 difab 3251 reuss2 3262 reupick 3266 raaan 3369 prss 3567 tpss 3576 prsspw 3583 prneimg 3592 uniin 3647 intun 3693 intpr 3694 brin 3858 brdif 3859 ssext 4012 pweqb 4014 opthg2 4030 copsex4g 4038 opelopabsb 4051 eqopab2b 4070 pwin 4073 pofun 4103 wetrep 4151 ordwe 4354 wessep 4356 reg3exmidlemwe 4357 elxp3 4450 soinxp 4466 relun 4512 inopab 4526 difopab 4527 inxp 4528 opelco2g 4562 cnvco 4579 dmin 4602 intasym 4771 asymref 4772 cnvdif 4792 xpm 4807 xp11m 4823 dfco2 4884 relssdmrn 4905 cnvpom 4927 xpcom 4931 dffun4 4980 dffun4f 4985 funun 5011 funcnveq 5030 fun11 5034 fununi 5035 imadif 5047 imainlem 5048 imain 5049 fnres 5083 fnopabg 5090 fun 5132 fin 5145 dff1o2 5206 brprcneu 5246 fsn 5411 dff1o6 5495 isotr 5535 brabvv 5630 eqoprab2b 5642 dfoprab3 5896 poxp 5932 cnvoprab 5934 f1od2 5935 brtpos2 5948 tfrlem7 6014 dfer2 6223 eqer 6254 iinerm 6294 brecop 6312 eroveu 6313 erovlem 6314 oviec 6328 mapval2 6365 xpcomco 6472 xpassen 6476 ssenen 6497 infmoti 6630 dfmq0qs 6891 dfplq0qs 6892 enq0enq 6893 enq0tr 6896 npsspw 6933 nqprdisj 7006 ltnqpr 7055 ltnqpri 7056 ltexprlemdisj 7068 addcanprg 7078 recexprlemdisj 7092 caucvgprprlemval 7150 addsrpr 7194 mulsrpr 7195 mulgt0sr 7226 addcnsr 7274 mulcnsr 7275 ltresr 7279 addvalex 7284 axcnre 7319 supinfneg 8978 infsupneg 8979 xrnemnf 9143 xrnepnf 9144 elfzuzb 9329 fzass4 9370 hashfacen 10075 rexanre 10480 infssuzex 10725 isprm3 10880 nnti 11234 |
Copyright terms: Public domain | W3C validator |