![]() |
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 431 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | anbi12.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | anbi2i 430 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitri 173 |
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: anbi12ci 434 ordir 729 orddi 732 dcan 841 3anbi123i 1092 an6 1215 xorcom 1276 trubifal 1304 truxortru 1307 truxorfal 1308 falxortru 1309 falxorfal 1310 nford 1456 nfand 1457 sbequ8 1724 sbanv 1766 sban 1826 sbbi 1830 sbnf2 1854 eu1 1922 2exeu 1989 2eu4 1990 sbabel 2200 neanior 2286 rexeqbii 2331 r19.26m 2438 reean 2472 reu5 2516 reu2 2723 reu3 2725 eqss 2954 unss 3111 ralunb 3118 ssin 3153 undi 3179 difundi 3183 indifdir 3187 inab 3199 difab 3200 reuss2 3211 reupick 3215 raaan 3321 prss 3511 tpss 3520 prsspw 3527 prneimg 3536 uniin 3591 intun 3637 intpr 3638 brin 3802 brdif 3803 ssext 3948 pweqb 3950 opthg2 3967 copsex4g 3975 opelopabsb 3988 eqopab2b 4007 pwin 4010 pofun 4040 elxp3 4337 soinxp 4353 relun 4397 inopab 4411 difopab 4412 inxp 4413 opelco2g 4446 cnvco 4463 dmin 4486 intasym 4652 asymref 4653 cnvdif 4673 xpm 4688 xp11m 4702 dfco2 4763 relssdmrn 4784 cnvpom 4803 xpcom 4807 dffun4 4856 dffun4f 4861 funun 4887 funcnveq 4905 fun11 4909 fununi 4910 imadif 4922 imainlem 4923 imain 4924 fnres 4958 fnopabg 4965 fun 5006 fin 5019 dff1o2 5074 brprcneu 5114 fsn 5278 dff1o6 5359 isotr 5399 brabvv 5493 eqoprab2b 5505 dfoprab3 5759 poxp 5794 brtpos2 5807 tfrlem7 5874 dfer2 6043 eqer 6074 iinerm 6114 brecop 6132 eroveu 6133 erovlem 6134 oviec 6148 xpcomco 6236 xpassen 6240 dfmq0qs 6412 dfplq0qs 6413 enq0enq 6414 enq0tr 6417 npsspw 6454 nqprdisj 6527 ltexprlemdisj 6580 addcanprg 6590 recexprlemdisj 6602 addsrpr 6673 mulsrpr 6674 mulgt0sr 6704 addcnsr 6731 mulcnsr 6732 ltresr 6736 axcnre 6765 xrnemnf 8469 xrnepnf 8470 elfzuzb 8654 fzass4 8695 |
Copyright terms: Public domain | W3C validator |