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 450 | 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 454 anbi12i 455 an12 550 anandi 579 pm5.53 791 pm5.75 946 3ancoma 969 3ioran 977 an6 1299 19.26-3an 1459 19.28h 1541 19.28 1542 eeeanv 1903 sb3an 1929 moanim 2071 nfrexdya 2468 r19.26-3 2560 r19.41 2584 rexcomf 2591 3reeanv 2599 cbvreu 2650 ceqsex3v 2723 rexab 2841 rexrab 2842 rmo4 2872 rmo3f 2876 reuind 2884 sbc3an 2965 rmo3 2995 ssrab 3170 rexun 3251 elin3 3262 inass 3281 unssdif 3306 indifdir 3327 difin2 3333 inrab2 3344 rabun2 3350 reuun2 3354 undif4 3420 rexsns 3558 rexdifsn 3650 2ralunsn 3720 iuncom4 3815 iunxiun 3889 inuni 4075 unidif0 4086 bnd2 4092 otth2 4158 copsexg 4161 copsex4g 4164 opeqsn 4169 opelopabsbALT 4176 elpwpwel 4391 suc11g 4467 rabxp 4571 opeliunxp 4589 xpundir 4591 xpiundi 4592 xpiundir 4593 brinxp2 4601 rexiunxp 4676 brres 4820 brresg 4822 dmres 4835 resiexg 4859 dminss 4948 imainss 4949 ssrnres 4976 elxp4 5021 elxp5 5022 cnvresima 5023 coundi 5035 resco 5038 imaco 5039 coiun 5043 coi1 5049 coass 5052 xpcom 5080 dffun2 5128 fncnv 5184 imadiflem 5197 imadif 5198 imainlem 5199 mptun 5249 fcnvres 5301 dff1o2 5365 dff1o3 5366 ffoss 5392 f11o 5393 brprcneu 5407 fvun2 5481 eqfnfv3 5513 respreima 5541 f1ompt 5564 fsn 5585 abrexco 5653 imaiun 5654 f1mpt 5665 dff1o6 5670 oprabid 5796 dfoprab2 5811 oprab4 5835 mpomptx 5855 opabex3d 6012 opabex3 6013 abexssex 6016 dfopab2 6080 dfoprab3s 6081 1stconst 6111 2ndconst 6112 xporderlem 6121 spc2ed 6123 f1od2 6125 brtpos2 6141 tpostpos 6154 tposmpo 6171 oviec 6528 mapsncnv 6582 dfixp 6587 domen 6638 mapsnen 6698 xpsnen 6708 xpcomco 6713 xpassen 6717 ltexpi 7138 dfmq0qs 7230 dfplq0qs 7231 enq0enq 7232 enq0ref 7234 enq0tr 7235 nqnq0pi 7239 prnmaxl 7289 prnminu 7290 suplocexprlemloc 7522 addsrpr 7546 mulsrpr 7547 suplocsrlemb 7607 addcnsr 7635 mulcnsr 7636 ltresr 7640 addvalex 7645 axprecex 7681 elnnz 9057 fnn0ind 9160 rexuz2 9369 qreccl 9427 rexrp 9457 elixx3g 9677 elfz2 9790 elfzuzb 9793 fznn 9862 elfz2nn0 9885 fznn0 9886 4fvwrd4 9910 elfzo2 9920 fzind2 10009 cvg1nlemres 10750 fsum2dlemstep 11196 modfsummod 11220 divalgb 11611 bezoutlemmain 11675 isprm2 11787 oddpwdc 11841 ntreq0 12290 cnnei 12390 txlm 12437 blres 12592 isms2 12612 dedekindicclemicc 12768 limcrcl 12785 bdcriota 13070 bj-peano4 13142 alsconv 13235 |
Copyright terms: Public domain | W3C validator |