![]() |
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 455 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: anbi2ci 459 anbi12i 460 bianassc 470 an12 561 anandi 590 pm5.53 803 pm5.75 964 3ancoma 987 3ioran 995 an6 1332 19.26-3an 1494 19.28h 1573 19.28 1574 eeeanv 1945 sb3an 1970 moanim 2112 nfrexdya 2526 r19.26-3 2620 r19.41 2645 rexcomf 2652 3reeanv 2661 cbvreu 2716 ceqsex3v 2794 rexab 2914 rexrab 2915 rmo4 2945 rmo3f 2949 reuind 2957 sbc3an 3039 rmo3 3069 ssrab 3248 rexun 3330 elin3 3341 inass 3360 unssdif 3385 indifdir 3406 difin2 3412 inrab2 3423 rabun2 3429 reuun2 3433 undif4 3500 rexdifpr 3635 rexsns 3646 rexdifsn 3739 2ralunsn 3813 iuncom4 3908 iunxiun 3983 inuni 4170 unidif0 4182 bnd2 4188 otth2 4256 copsexg 4259 copsex4g 4262 opeqsn 4267 opelopabsbALT 4274 elpwpwel 4490 suc11g 4571 rabxp 4678 opeliunxp 4696 xpundir 4698 xpiundi 4699 xpiundir 4700 brinxp2 4708 rexiunxp 4784 brres 4928 brresg 4930 dmres 4943 resiexg 4967 dminss 5058 imainss 5059 ssrnres 5086 elxp4 5131 elxp5 5132 cnvresima 5133 coundi 5145 resco 5148 imaco 5149 coiun 5153 coi1 5159 coass 5162 xpcom 5190 dffun2 5241 fncnv 5297 imadiflem 5310 imadif 5311 imainlem 5312 mptun 5362 fcnvres 5414 dff1o2 5481 dff1o3 5482 ffoss 5508 f11o 5509 brprcneu 5523 fvun2 5599 eqfnfv3 5631 respreima 5660 f1ompt 5683 fsn 5704 abrexco 5776 imaiun 5777 f1mpt 5788 dff1o6 5793 oprabid 5923 dfoprab2 5938 oprab4 5962 mpomptx 5982 opabex3d 6140 opabex3 6141 abexssex 6144 dfopab2 6208 dfoprab3s 6209 1stconst 6240 2ndconst 6241 xporderlem 6250 spc2ed 6252 f1od2 6254 brtpos2 6270 tpostpos 6283 tposmpo 6300 oviec 6659 mapsncnv 6713 dfixp 6718 domen 6769 mapsnen 6829 xpsnen 6839 xpcomco 6844 xpassen 6848 ltexpi 7354 dfmq0qs 7446 dfplq0qs 7447 enq0enq 7448 enq0ref 7450 enq0tr 7451 nqnq0pi 7455 prnmaxl 7505 prnminu 7506 suplocexprlemloc 7738 addsrpr 7762 mulsrpr 7763 suplocsrlemb 7823 addcnsr 7851 mulcnsr 7852 ltresr 7856 addvalex 7861 axprecex 7897 elnnz 9281 fnn0ind 9387 rexuz2 9599 qreccl 9660 rexrp 9694 elixx3g 9919 elfz2 10033 elfzuzb 10037 fznn 10107 elfz2nn0 10130 fznn0 10131 4fvwrd4 10158 elfzo2 10168 fzind2 10257 cvg1nlemres 11012 fsum2dlemstep 11460 modfsummod 11484 fprodseq 11609 divalgb 11948 bezoutlemmain 12017 isprm2 12135 oddpwdc 12192 prdsex 12740 xpscf 12789 issubg3 13097 releqgg 13125 eqgex 13126 imasabl 13234 dfrhm2 13465 ntreq0 14016 cnnei 14116 txlm 14163 blres 14318 isms2 14338 dedekindicclemicc 14494 limcrcl 14511 bdcriota 15019 bj-peano4 15091 alsconv 15213 |
Copyright terms: Public domain | W3C validator |