Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > anbi1i | Unicode version |
Description: Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.) |
Ref | Expression |
---|---|
bi.aa |
Ref | Expression |
---|---|
anbi1i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi.aa | . . 3 | |
2 | 1 | a1i 9 | . 2 |
3 | 2 | pm5.32ri 451 | 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: anbi2ci 455 anbi12i 456 an12 551 anandi 580 pm5.53 792 pm5.75 947 3ancoma 970 3ioran 978 an6 1303 19.26-3an 1463 19.28h 1542 19.28 1543 eeeanv 1913 sb3an 1938 moanim 2080 nfrexdya 2493 r19.26-3 2587 r19.41 2612 rexcomf 2619 3reeanv 2627 cbvreu 2678 ceqsex3v 2754 rexab 2874 rexrab 2875 rmo4 2905 rmo3f 2909 reuind 2917 sbc3an 2998 rmo3 3028 ssrab 3206 rexun 3287 elin3 3298 inass 3317 unssdif 3342 indifdir 3363 difin2 3369 inrab2 3380 rabun2 3386 reuun2 3390 undif4 3456 rexdifpr 3588 rexsns 3599 rexdifsn 3692 2ralunsn 3762 iuncom4 3857 iunxiun 3931 inuni 4117 unidif0 4129 bnd2 4135 otth2 4202 copsexg 4205 copsex4g 4208 opeqsn 4213 opelopabsbALT 4220 elpwpwel 4436 suc11g 4517 rabxp 4624 opeliunxp 4642 xpundir 4644 xpiundi 4645 xpiundir 4646 brinxp2 4654 rexiunxp 4729 brres 4873 brresg 4875 dmres 4888 resiexg 4912 dminss 5001 imainss 5002 ssrnres 5029 elxp4 5074 elxp5 5075 cnvresima 5076 coundi 5088 resco 5091 imaco 5092 coiun 5096 coi1 5102 coass 5105 xpcom 5133 dffun2 5181 fncnv 5237 imadiflem 5250 imadif 5251 imainlem 5252 mptun 5302 fcnvres 5354 dff1o2 5420 dff1o3 5421 ffoss 5447 f11o 5448 brprcneu 5462 fvun2 5536 eqfnfv3 5568 respreima 5596 f1ompt 5619 fsn 5640 abrexco 5710 imaiun 5711 f1mpt 5722 dff1o6 5727 oprabid 5854 dfoprab2 5869 oprab4 5893 mpomptx 5913 opabex3d 6070 opabex3 6071 abexssex 6074 dfopab2 6138 dfoprab3s 6139 1stconst 6169 2ndconst 6170 xporderlem 6179 spc2ed 6181 f1od2 6183 brtpos2 6199 tpostpos 6212 tposmpo 6229 oviec 6587 mapsncnv 6641 dfixp 6646 domen 6697 mapsnen 6757 xpsnen 6767 xpcomco 6772 xpassen 6776 ltexpi 7258 dfmq0qs 7350 dfplq0qs 7351 enq0enq 7352 enq0ref 7354 enq0tr 7355 nqnq0pi 7359 prnmaxl 7409 prnminu 7410 suplocexprlemloc 7642 addsrpr 7666 mulsrpr 7667 suplocsrlemb 7727 addcnsr 7755 mulcnsr 7756 ltresr 7760 addvalex 7765 axprecex 7801 elnnz 9178 fnn0ind 9281 rexuz2 9493 qreccl 9552 rexrp 9584 elixx3g 9806 elfz2 9920 elfzuzb 9923 fznn 9992 elfz2nn0 10015 fznn0 10016 4fvwrd4 10043 elfzo2 10053 fzind2 10142 cvg1nlemres 10889 fsum2dlemstep 11335 modfsummod 11359 fprodseq 11484 divalgb 11820 bezoutlemmain 11886 isprm2 11998 oddpwdc 12053 ntreq0 12574 cnnei 12674 txlm 12721 blres 12876 isms2 12896 dedekindicclemicc 13052 limcrcl 13069 bdcriota 13500 bj-peano4 13572 alsconv 13690 |
Copyright terms: Public domain | W3C validator |