Theorem anbi2i 461

Description: Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
bi.aa	|- ( ph <-> ps )

Assertion

Ref	Expression
anbi2i	|- ( ( ch /\ ph ) <-> ( ch /\ ps ) )

Proof of Theorem anbi2i

Step	Hyp	Ref	Expression
1		bi.aa	. . 3 |- ( ph <-> ps )
2	1	a1i 9	. 2 |- ( ch -> ( ph <-> ps ) )
3	2	pm5.32i 458	1 |- ( ( ch /\ ph ) <-> ( ch /\ ps ) )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi12i  464  bianass  473  mpan10  478  an4  592  an42  593  anandir  599  dcim  853  19.27h  1613  19.27  1614  19.41  1738  sbcof2  1863  sbidm  1904  sb6  1941  3exdistr  1971  4exdistr  1972  2sb5  2043  2sb5rf  2049  sbel2x  2058  eu2  2131  euan  2143  sbmo  2146  mo4f  2147  eu4  2149  moanim  2161  2eu4  2180  clelab  2366  nonconne  2432  r2exf  2568  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  reu2  3014  reu6  3015  reu4  3020  reu7  3021  rmo3f  3023  rmo4f  3024  2rmorex  3032  rmo3  3144  raldifb  3369  inass  3441  dfss4st  3464  ssddif  3465  difin  3468  invdif  3473  indif  3474  indi  3478  difundi  3483  difindiss  3485  inssdif0imOLD  3593  rexdifpr  3737  ssdifsn  3842  unipr  3949  uniun  3954  uniin  3955  iunin2  4076  iindif2m  4080  iinin2m  4081  elpwpw  4099  unidif0  4306  mss  4368  eqvinop  4385  opcom  4393  opeqsn  4395  uniuni  4599  zfinf2  4738  elomssom  4754  fconstmpt  4824  opeliunxp  4832  xpundi  4833  elvvv  4840  xpiindim  4919  elcnv2  4960  cnvuni  4968  dmuni  4993  opelres  5070  restidsing  5122  elima3  5136  imai  5146  imainss  5206  ssrnres  5233  cnvresima  5280  mptpreima  5284  coundir  5293  rnco  5297  coass  5309  relrelss  5317  dffun2  5390  dffun4  5391  dffun6f  5393  dffun4f  5396  dffun7  5407  dffun8  5408  dffun9  5409  svrelfun  5449  fncnv  5450  funcnvuni  5453  dfmpt3  5509  fintm  5580  fin  5581  dff12  5600  fores  5628  dff1o4  5650  eqfnfv3  5811  unpreima  5836  ffnfvf  5870  dff13f  5979  ffnov  6195  eqfnov  6198  foov  6239  opabex3d  6354  opabex3  6355  uchoice  6375  mpoxopovel  6517  tpostpos  6540  dfsmo2  6563  tfr1onlemaccex  6624  tfrcllembxssdm  6632  tfrcllemaccex  6637  tfrcllemres  6638  tfrcldm  6639  erinxp  6888  mapsncnv  6983  cbvixp  7003  ixpin  7011  ixpiinm  7012  mptelixpg  7022  elixpsn  7023  ixpsnf1o  7024  mapsnen  7106  xpassen  7134  2omap  7324  2omotaplemap  7629  distrnqg  7760  subhalfnqq  7787  enq0enq  7804  enq0sym  7805  enq0tr  7807  addnq0mo  7820  mulnq0mo  7821  distrnq0  7832  prarloc  7876  nqprrnd  7916  ltexprlemopl  7974  ltexprlemlol  7975  ltexprlemopu  7976  ltexprlemupu  7977  ltexprlemdisj  7979  ltexprlemloc  7980  recexprlemdisj  8003  caucvgprprlemell  8058  caucvgprprlemelu  8059  addsrmo  8116  mulsrmo  8117  opelreal  8200  axcaucvglemres  8272  axpre-suploc  8275  elnnz  9663  elznn0nn  9667  zltlen  9733  suprzclex  9754  peano2uz2  9763  peano5uzti  9764  qltlen  10055  elfzuzb  10438  4fvwrd4  10563  fzind2  10674  cvg1nlemres  11772  rexfiuz  11776  cbvsum  12150  mertenslem2  12327  mertensabs  12328  cbvprod  12349  prodmodc  12369  fprodseq  12374  ndvdssub  12721  bitsmod  12747  nnwosdc  12840  isprm2  12919  isprm4  12921  hashdvds  13027  xpscf  13726  fngzsum  13766  gzsumvalx  13767  isnsg2  14064  isnsg4  14073  isrhm  14573  issubrng  14615  subsubrng2  14631  subsubrg2  14662  psrbaglefifi  15175  isbasis2g  15288  tgval2  15294  elcncf1di  15822  dedekindicclemicc  15875  dedekindicc  15876  plyco  16002  isclwwlk  16857  clwwlknon2x  16898  iseupthf1o  16911  idjudju  17269  alsanmo  17375  ralsanmo  17376  2alsraln0m  17382  2alsraln0idm  17383