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 452 | 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 456 anbi12i 457 bianassc 467 an12 556 anandi 585 pm5.53 797 pm5.75 957 3ancoma 980 3ioran 988 an6 1316 19.26-3an 1476 19.28h 1555 19.28 1556 eeeanv 1926 sb3an 1951 moanim 2093 nfrexdya 2506 r19.26-3 2600 r19.41 2625 rexcomf 2632 3reeanv 2640 cbvreu 2694 ceqsex3v 2772 rexab 2892 rexrab 2893 rmo4 2923 rmo3f 2927 reuind 2935 sbc3an 3016 rmo3 3046 ssrab 3225 rexun 3307 elin3 3318 inass 3337 unssdif 3362 indifdir 3383 difin2 3389 inrab2 3400 rabun2 3406 reuun2 3410 undif4 3477 rexdifpr 3611 rexsns 3622 rexdifsn 3715 2ralunsn 3785 iuncom4 3880 iunxiun 3954 inuni 4141 unidif0 4153 bnd2 4159 otth2 4226 copsexg 4229 copsex4g 4232 opeqsn 4237 opelopabsbALT 4244 elpwpwel 4460 suc11g 4541 rabxp 4648 opeliunxp 4666 xpundir 4668 xpiundi 4669 xpiundir 4670 brinxp2 4678 rexiunxp 4753 brres 4897 brresg 4899 dmres 4912 resiexg 4936 dminss 5025 imainss 5026 ssrnres 5053 elxp4 5098 elxp5 5099 cnvresima 5100 coundi 5112 resco 5115 imaco 5116 coiun 5120 coi1 5126 coass 5129 xpcom 5157 dffun2 5208 fncnv 5264 imadiflem 5277 imadif 5278 imainlem 5279 mptun 5329 fcnvres 5381 dff1o2 5447 dff1o3 5448 ffoss 5474 f11o 5475 brprcneu 5489 fvun2 5563 eqfnfv3 5595 respreima 5624 f1ompt 5647 fsn 5668 abrexco 5738 imaiun 5739 f1mpt 5750 dff1o6 5755 oprabid 5885 dfoprab2 5900 oprab4 5924 mpomptx 5944 opabex3d 6100 opabex3 6101 abexssex 6104 dfopab2 6168 dfoprab3s 6169 1stconst 6200 2ndconst 6201 xporderlem 6210 spc2ed 6212 f1od2 6214 brtpos2 6230 tpostpos 6243 tposmpo 6260 oviec 6619 mapsncnv 6673 dfixp 6678 domen 6729 mapsnen 6789 xpsnen 6799 xpcomco 6804 xpassen 6808 ltexpi 7299 dfmq0qs 7391 dfplq0qs 7392 enq0enq 7393 enq0ref 7395 enq0tr 7396 nqnq0pi 7400 prnmaxl 7450 prnminu 7451 suplocexprlemloc 7683 addsrpr 7707 mulsrpr 7708 suplocsrlemb 7768 addcnsr 7796 mulcnsr 7797 ltresr 7801 addvalex 7806 axprecex 7842 elnnz 9222 fnn0ind 9328 rexuz2 9540 qreccl 9601 rexrp 9633 elixx3g 9858 elfz2 9972 elfzuzb 9975 fznn 10045 elfz2nn0 10068 fznn0 10069 4fvwrd4 10096 elfzo2 10106 fzind2 10195 cvg1nlemres 10949 fsum2dlemstep 11397 modfsummod 11421 fprodseq 11546 divalgb 11884 bezoutlemmain 11953 isprm2 12071 oddpwdc 12128 ntreq0 12926 cnnei 13026 txlm 13073 blres 13228 isms2 13248 dedekindicclemicc 13404 limcrcl 13421 bdcriota 13918 bj-peano4 13990 alsconv 14109 |
Copyright terms: Public domain | W3C validator |