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 453 | . 2 |
3 | anbi12.2 | . . 3 | |
4 | 3 | anbi2i 452 | . 2 |
5 | 2, 4 | bitri 183 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 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: anbi12ci 456 ordir 806 orddi 809 dcan 918 3anbi123i 1170 an6 1299 xorcom 1366 trubifal 1394 truxortru 1397 truxorfal 1398 falxortru 1399 falxorfal 1400 nford 1546 nfand 1547 sbequ8 1819 sbanv 1861 sban 1928 sbbi 1932 sbnf2 1956 eu1 2024 2exeu 2091 2eu4 2092 sbabel 2307 neanior 2395 rexeqbii 2448 r19.26m 2563 reean 2599 reu5 2643 reu2 2872 reu3 2874 eqss 3112 unss 3250 ralunb 3257 ssin 3298 undi 3324 difundi 3328 indifdir 3332 inab 3344 difab 3345 reuss2 3356 reupick 3360 raaan 3469 prss 3676 tpss 3685 prsspw 3692 prneimg 3701 uniin 3756 intun 3802 intpr 3803 disjiun 3924 brin 3980 brdif 3981 ssext 4143 pweqb 4145 opthg2 4161 copsex4g 4169 opelopabsb 4182 eqopab2b 4201 pwin 4204 pofun 4234 wetrep 4282 ordwe 4490 wessep 4492 reg3exmidlemwe 4493 elxp3 4593 soinxp 4609 relun 4656 inopab 4671 difopab 4672 inxp 4673 opelco2g 4707 cnvco 4724 dmin 4747 intasym 4923 asymref 4924 cnvdif 4945 xpm 4960 xp11m 4977 dfco2 5038 relssdmrn 5059 cnvpom 5081 xpcom 5085 dffun4 5134 dffun4f 5139 funun 5167 funcnveq 5186 fun11 5190 fununi 5191 imadif 5203 imainlem 5204 imain 5205 fnres 5239 fnopabg 5246 fun 5295 fin 5309 dff1o2 5372 brprcneu 5414 fsn 5592 dff1o6 5677 isotr 5717 brabvv 5817 eqoprab2b 5829 dfoprab3 6089 poxp 6129 cnvoprab 6131 f1od2 6132 brtpos2 6148 tfrlem7 6214 dfer2 6430 eqer 6461 iinerm 6501 brecop 6519 eroveu 6520 erovlem 6521 oviec 6535 mapval2 6572 ixpin 6617 xpcomco 6720 xpassen 6724 ssenen 6745 sbthlemi10 6854 infmoti 6915 dfmq0qs 7237 dfplq0qs 7238 enq0enq 7239 enq0tr 7242 npsspw 7279 nqprdisj 7352 ltnqpr 7401 ltnqpri 7402 ltexprlemdisj 7414 addcanprg 7424 recexprlemdisj 7438 caucvgprprlemval 7496 addsrpr 7553 mulsrpr 7554 mulgt0sr 7586 addcnsr 7642 mulcnsr 7643 ltresr 7647 addvalex 7652 axcnre 7689 axpre-suploc 7710 supinfneg 9390 infsupneg 9391 xrnemnf 9564 xrnepnf 9565 elfzuzb 9800 fzass4 9842 hashfacen 10579 rexanre 10992 cbvprod 11327 infssuzex 11642 isprm3 11799 tgval2 12220 epttop 12259 cnnei 12401 txuni2 12425 txbas 12427 txdis1cn 12447 xmeterval 12604 dedekindicc 12780 bj-stan 12955 nnti 13191 |
Copyright terms: Public domain | W3C validator |