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 ) )

Syntax hints:   /\ wa 104   <-> wb 105

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:  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  inssdif0im  3591  rexdifpr  3733  ssdifsn  3837  unipr  3944  uniun  3949  uniin  3950  iunin2  4071  iindif2m  4075  iinin2m  4076  elpwpw  4094  unidif0  4299  mss  4361  eqvinop  4378  opcom  4386  opeqsn  4388  uniuni  4592  zfinf2  4731  elomssom  4747  fconstmpt  4817  opeliunxp  4825  xpundi  4826  elvvv  4833  xpiindim  4912  elcnv2  4953  cnvuni  4961  dmuni  4986  opelres  5063  restidsing  5114  elima3  5128  imai  5138  imainss  5198  ssrnres  5225  cnvresima  5272  mptpreima  5276  coundir  5285  rnco  5289  coass  5301  relrelss  5309  dffun2  5382  dffun4  5383  dffun6f  5385  dffun4f  5388  dffun7  5399  dffun8  5400  dffun9  5401  svrelfun  5441  fncnv  5442  funcnvuni  5445  dfmpt3  5501  fintm  5572  fin  5573  dff12  5592  fores  5620  dff1o4  5642  eqfnfv3  5799  unpreima  5824  ffnfvf  5858  dff13f  5966  ffnov  6182  eqfnov  6185  foov  6226  opabex3d  6340  opabex3  6341  uchoice  6361  mpoxopovel  6502  tpostpos  6525  dfsmo2  6548  tfr1onlemaccex  6609  tfrcllembxssdm  6617  tfrcllemaccex  6622  tfrcllemres  6623  tfrcldm  6624  erinxp  6873  mapsncnv  6967  cbvixp  6987  ixpin  6995  ixpiinm  6996  mptelixpg  7006  elixpsn  7007  ixpsnf1o  7008  mapsnen  7090  xpassen  7118  2omap  7308  2omotaplemap  7613  distrnqg  7744  subhalfnqq  7771  enq0enq  7788  enq0sym  7789  enq0tr  7791  addnq0mo  7804  mulnq0mo  7805  distrnq0  7816  prarloc  7860  nqprrnd  7900  ltexprlemopl  7958  ltexprlemlol  7959  ltexprlemopu  7960  ltexprlemupu  7961  ltexprlemdisj  7963  ltexprlemloc  7964  recexprlemdisj  7987  caucvgprprlemell  8042  caucvgprprlemelu  8043  addsrmo  8100  mulsrmo  8101  opelreal  8184  axcaucvglemres  8256  axpre-suploc  8259  elnnz  9633  elznn0nn  9637  zltlen  9703  suprzclex  9723  peano2uz2  9732  peano5uzti  9733  qltlen  10019  elfzuzb  10401  4fvwrd4  10525  fzind2  10636  cvg1nlemres  11729  rexfiuz  11733  cbvsum  12104  mertenslem2  12281  mertensabs  12282  cbvprod  12303  prodmodc  12323  fprodseq  12328  ndvdssub  12675  bitsmod  12701  nnwosdc  12794  isprm2  12873  isprm4  12875  hashdvds  12977  xpscf  13645  fngzsum  13685  gzsumvalx  13686  isnsg2  13983  isnsg4  13992  isrhm  14438  issubrng  14480  subsubrng2  14496  subsubrg2  14527  isbasis2g  15069  tgval2  15075  elcncf1di  15603  dedekindicclemicc  15656  dedekindicc  15657  plyco  15783  isclwwlk  16549  clwwlknon2x  16590  iseupthf1o  16603