Theorem anbi2i 453

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 450	1 |- ( ( ch /\ ph ) <-> ( ch /\ ps ) )

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:  anbi12i  456  mpan10  466  an4  576  an42  577  anandir  581  dcim  831  19.27h  1548  19.27  1549  19.41  1674  sbcof2  1798  sbidm  1839  sb6  1874  3exdistr  1903  4exdistr  1904  2sb5  1971  2sb5rf  1977  sbel2x  1986  eu2  2058  euan  2070  sbmo  2073  mo4f  2074  eu4  2076  moanim  2088  2eu4  2107  clelab  2292  nonconne  2348  r2exf  2484  ceqsex3v  2768  ceqsex4v  2769  ceqsex8v  2771  reu2  2914  reu6  2915  reu4  2920  reu7  2921  rmo3f  2923  rmo4f  2924  2rmorex  2932  rmo3  3042  raldifb  3262  inass  3332  dfss4st  3355  ssddif  3356  difin  3359  invdif  3364  indif  3365  indi  3369  difundi  3374  difindiss  3376  inssdif0im  3476  rexdifpr  3604  ssdifsn  3704  unipr  3803  uniun  3808  uniin  3809  iunin2  3929  iindif2m  3933  iinin2m  3934  elpwpw  3952  unidif0  4146  mss  4204  eqvinop  4221  opcom  4228  opeqsn  4230  uniuni  4429  zfinf2  4566  elomssom  4582  fconstmpt  4651  opeliunxp  4659  xpundi  4660  elvvv  4667  xpiindim  4741  elcnv2  4782  cnvuni  4790  dmuni  4814  opelres  4889  elima3  4953  imai  4960  imainss  5019  ssrnres  5046  cnvresima  5093  mptpreima  5097  coundir  5106  rnco  5110  coass  5122  relrelss  5130  dffun2  5198  dffun4  5199  dffun6f  5201  dffun4f  5204  dffun7  5215  dffun8  5216  dffun9  5217  svrelfun  5253  fncnv  5254  funcnvuni  5257  dfmpt3  5310  fintm  5373  fin  5374  dff12  5392  fores  5419  dff1o4  5440  eqfnfv3  5585  unpreima  5610  ffnfvf  5644  dff13f  5738  ffnov  5946  eqfnov  5948  foov  5988  opabex3d  6089  opabex3  6090  mpoxopovel  6209  tpostpos  6232  dfsmo2  6255  tfr1onlemaccex  6316  tfrcllembxssdm  6324  tfrcllemaccex  6329  tfrcllemres  6330  tfrcldm  6331  erinxp  6575  mapsncnv  6661  cbvixp  6681  ixpin  6689  ixpiinm  6690  mptelixpg  6700  elixpsn  6701  ixpsnf1o  6702  mapsnen  6777  xpassen  6796  distrnqg  7328  subhalfnqq  7355  enq0enq  7372  enq0sym  7373  enq0tr  7375  addnq0mo  7388  mulnq0mo  7389  distrnq0  7400  prarloc  7444  nqprrnd  7484  ltexprlemopl  7542  ltexprlemlol  7543  ltexprlemopu  7544  ltexprlemupu  7545  ltexprlemdisj  7547  ltexprlemloc  7548  recexprlemdisj  7571  caucvgprprlemell  7626  caucvgprprlemelu  7627  addsrmo  7684  mulsrmo  7685  opelreal  7768  axcaucvglemres  7840  axpre-suploc  7843  elnnz  9201  elznn0nn  9205  zltlen  9269  suprzclex  9289  peano2uz2  9298  peano5uzti  9299  qltlen  9578  elfzuzb  9954  4fvwrd4  10075  fzind2  10174  cvg1nlemres  10927  rexfiuz  10931  cbvsum  11301  mertenslem2  11477  mertensabs  11478  cbvprod  11499  prodmodc  11519  fprodseq  11524  ndvdssub  11867  nnwosdc  11972  isprm2  12049  isprm4  12051  hashdvds  12153  isbasis2g  12683  tgval2  12691  elcncf1di  13206  dedekindicclemicc  13250  dedekindicc  13251