![]() |
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 428 |
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 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: anbi2ci 432 anbi12i 433 an12 495 anandi 524 pm5.53 714 pm5.75 868 3ancoma 891 3ioran 899 an6 1215 19.26-3an 1369 19.28h 1451 19.28 1452 eeeanv 1805 sb3an 1829 moanim 1971 nfrexdya 2353 r19.26-3 2437 r19.41 2459 rexcomf 2466 3reeanv 2474 cbvreu 2525 ceqsex3v 2590 rexab 2697 rexrab 2698 rmo4 2728 reuind 2738 rmo3 2843 ssrab 3012 rexun 3117 elin3 3122 inass 3141 unssdif 3166 indifdir 3187 difin2 3193 inrab2 3204 rabun2 3210 reuun2 3214 undif4 3278 rexsns 3400 rexsnsOLD 3401 rexdifsn 3490 2ralunsn 3560 iuncom4 3655 iunxiun 3727 inuni 3900 unidif0 3911 bnd2 3917 otth2 3969 copsexg 3972 copsex4g 3975 opeqsn 3980 opelopabsbALT 3987 suc11g 4235 rabxp 4323 opeliunxp 4338 xpundir 4340 xpiundi 4341 xpiundir 4342 brinxp2 4350 rexiunxp 4421 brres 4561 brresg 4563 dmres 4575 resiexg 4596 dminss 4681 imainss 4682 ssrnres 4706 elxp4 4751 elxp5 4752 cnvresima 4753 coundi 4765 resco 4768 imaco 4769 coiun 4773 coi1 4779 coass 4782 xpcom 4807 dffun2 4855 fncnv 4908 imadiflem 4921 imadif 4922 imainlem 4923 mptun 4972 fcnvres 5016 dff1o2 5074 dff1o3 5075 ffoss 5101 f11o 5102 brprcneu 5114 fvun2 5183 eqfnfv3 5210 respreima 5238 f1ompt 5263 fsn 5278 abrexco 5341 imaiun 5342 f1mpt 5353 dff1o6 5359 oprabid 5480 dfoprab2 5494 oprab4 5517 mpt2mptx 5537 opabex3d 5690 opabex3 5691 abexssex 5694 dfopab2 5757 dfoprab3s 5758 1stconst 5784 2ndconst 5785 xporderlem 5793 brtpos2 5807 tpostpos 5820 tposmpt2 5837 oviec 6148 domen 6168 xpsnen 6231 xpcomco 6236 xpassen 6240 ltexpi 6321 dfmq0qs 6412 dfplq0qs 6413 enq0enq 6414 enq0ref 6416 enq0tr 6417 nqnq0pi 6421 prnmaxl 6471 prnminu 6472 addsrpr 6673 mulsrpr 6674 addcnsr 6731 mulcnsr 6732 ltresr 6736 axprecex 6764 elnnz 8031 fnn0ind 8130 rexuz2 8300 qreccl 8351 rexrp 8380 elixx3g 8540 elfz2 8651 elfzuzb 8654 fznn 8721 elfz2nn0 8743 fznn0 8744 4fvwrd4 8767 elfzo2 8777 fzind2 8865 bdcriota 9338 bj-peano4 9415 alsconv 9453 |
Copyright terms: Public domain | W3C validator |