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 442 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 102 wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: anbi2ci 446 anbi12i 447 an12 525 anandi 554 pm5.53 748 pm5.75 903 3ancoma 926 3ioran 934 an6 1252 19.26-3an 1412 19.28h 1494 19.28 1495 eeeanv 1849 sb3an 1873 moanim 2015 nfrexdya 2401 r19.26-3 2487 r19.41 2509 rexcomf 2516 3reeanv 2524 cbvreu 2575 ceqsex3v 2641 rexab 2754 rexrab 2755 rmo4 2785 reuind 2795 sbc3an 2875 rmo3 2905 ssrab 3072 rexun 3152 elin3 3157 inass 3176 unssdif 3199 indifdir 3220 difin2 3226 inrab2 3237 rabun2 3243 reuun2 3247 undif4 3306 rexsns 3432 rexdifsn 3521 2ralunsn 3590 iuncom4 3685 iunxiun 3757 inuni 3930 unidif0 3941 bnd2 3947 otth2 3996 copsexg 3999 copsex4g 4002 opeqsn 4007 opelopabsbALT 4014 suc11g 4300 rabxp 4398 opeliunxp 4413 xpundir 4415 xpiundi 4416 xpiundir 4417 brinxp2 4425 rexiunxp 4496 brres 4636 brresg 4638 dmres 4650 resiexg 4673 dminss 4758 imainss 4759 ssrnres 4783 elxp4 4828 elxp5 4829 cnvresima 4830 coundi 4842 resco 4845 imaco 4846 coiun 4850 coi1 4856 coass 4859 xpcom 4884 dffun2 4932 fncnv 4985 imadiflem 4998 imadif 4999 imainlem 5000 mptun 5049 fcnvres 5093 dff1o2 5151 dff1o3 5152 ffoss 5178 f11o 5179 brprcneu 5191 fvun2 5261 eqfnfv3 5288 respreima 5316 f1ompt 5341 fsn 5356 abrexco 5419 imaiun 5420 f1mpt 5431 dff1o6 5436 oprabid 5557 dfoprab2 5572 oprab4 5595 mpt2mptx 5615 opabex3d 5768 opabex3 5769 abexssex 5772 dfopab2 5835 dfoprab3s 5836 1stconst 5862 2ndconst 5863 xporderlem 5872 spc2ed 5874 f1od2 5876 brtpos2 5889 tpostpos 5902 tposmpt2 5919 oviec 6235 domen 6255 xpsnen 6318 xpcomco 6323 xpassen 6327 ltexpi 6527 dfmq0qs 6619 dfplq0qs 6620 enq0enq 6621 enq0ref 6623 enq0tr 6624 nqnq0pi 6628 prnmaxl 6678 prnminu 6679 addsrpr 6922 mulsrpr 6923 addcnsr 7002 mulcnsr 7003 ltresr 7007 addvalex 7012 axprecex 7046 elnnz 8361 fnn0ind 8463 rexuz2 8669 qreccl 8727 rexrp 8756 elixx3g 8924 elfz2 9036 elfzuzb 9039 fznn 9106 elfz2nn0 9128 fznn0 9129 4fvwrd4 9150 elfzo2 9160 fzind2 9248 cvg1nlemres 9871 divalgb 10325 bezoutlemmain 10387 isprm2 10499 oddpwdc 10552 bdcriota 10674 bj-peano4 10750 alsconv 10791 |
Copyright terms: Public domain | W3C validator |