![]() |
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 448 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: anbi2ci 452 anbi12i 453 an12 533 anandi 562 pm5.53 774 pm5.75 927 3ancoma 950 3ioran 958 an6 1280 19.26-3an 1440 19.28h 1522 19.28 1523 eeeanv 1881 sb3an 1905 moanim 2047 nfrexdya 2442 r19.26-3 2534 r19.41 2558 rexcomf 2565 3reeanv 2573 cbvreu 2624 ceqsex3v 2697 rexab 2813 rexrab 2814 rmo4 2844 rmo3f 2848 reuind 2856 sbc3an 2936 rmo3 2966 ssrab 3139 rexun 3220 elin3 3231 inass 3250 unssdif 3275 indifdir 3296 difin2 3302 inrab2 3313 rabun2 3319 reuun2 3323 undif4 3389 rexsns 3527 rexdifsn 3619 2ralunsn 3689 iuncom4 3784 iunxiun 3858 inuni 4038 unidif0 4049 bnd2 4055 otth2 4121 copsexg 4124 copsex4g 4127 opeqsn 4132 opelopabsbALT 4139 elpwpwel 4354 suc11g 4430 rabxp 4534 opeliunxp 4552 xpundir 4554 xpiundi 4555 xpiundir 4556 brinxp2 4564 rexiunxp 4639 brres 4781 brresg 4783 dmres 4796 resiexg 4820 dminss 4909 imainss 4910 ssrnres 4937 elxp4 4982 elxp5 4983 cnvresima 4984 coundi 4996 resco 4999 imaco 5000 coiun 5004 coi1 5010 coass 5013 xpcom 5041 dffun2 5089 fncnv 5145 imadiflem 5158 imadif 5159 imainlem 5160 mptun 5210 fcnvres 5262 dff1o2 5326 dff1o3 5327 ffoss 5353 f11o 5354 brprcneu 5366 fvun2 5440 eqfnfv3 5472 respreima 5500 f1ompt 5523 fsn 5544 abrexco 5612 imaiun 5613 f1mpt 5624 dff1o6 5629 oprabid 5755 dfoprab2 5770 oprab4 5794 mpomptx 5814 opabex3d 5970 opabex3 5971 abexssex 5974 dfopab2 6038 dfoprab3s 6039 1stconst 6069 2ndconst 6070 xporderlem 6079 spc2ed 6081 f1od2 6083 brtpos2 6099 tpostpos 6112 tposmpo 6129 oviec 6486 mapsncnv 6540 dfixp 6545 domen 6596 mapsnen 6656 xpsnen 6665 xpcomco 6670 xpassen 6674 ltexpi 7086 dfmq0qs 7178 dfplq0qs 7179 enq0enq 7180 enq0ref 7182 enq0tr 7183 nqnq0pi 7187 prnmaxl 7237 prnminu 7238 addsrpr 7481 mulsrpr 7482 addcnsr 7562 mulcnsr 7563 ltresr 7567 addvalex 7572 axprecex 7608 elnnz 8961 fnn0ind 9064 rexuz2 9271 qreccl 9329 rexrp 9358 elixx3g 9570 elfz2 9683 elfzuzb 9686 fznn 9755 elfz2nn0 9778 fznn0 9779 4fvwrd4 9803 elfzo2 9813 fzind2 9902 cvg1nlemres 10642 fsum2dlemstep 11088 modfsummod 11112 divalgb 11463 bezoutlemmain 11525 isprm2 11637 oddpwdc 11690 ntreq0 12137 cnnei 12236 txlm 12283 blres 12416 isms2 12436 limcrcl 12576 bdcriota 12760 bj-peano4 12832 alsconv 12922 |
Copyright terms: Public domain | W3C validator |