Theorem anbi2i 444

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

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:  anbi12i  447  mpan10  457  an4  550  an42  551  anandir  555  dcim  817  19.27h  1492  19.27  1493  19.41  1616  sbcof2  1731  sbidm  1772  sb6  1807  3exdistr  1833  4exdistr  1834  2sb5  1900  2sb5rf  1906  sbel2x  1915  eu2  1985  euan  1997  sbmo  2000  mo4f  2001  eu4  2003  moanim  2015  2eu4  2034  clelab  2203  nonconne  2257  r2exf  2384  ceqsex3v  2641  ceqsex4v  2642  ceqsex8v  2644  reu2  2780  reu6  2781  reu4  2786  reu7  2787  2rmorex  2796  rmo3  2905  raldifb  3112  inass  3176  ssddif  3198  difin  3201  invdif  3206  indif  3207  indi  3211  difundi  3216  difindiss  3218  inssdif0im  3311  unipr  3615  uniun  3620  uniin  3621  iunin2  3741  iindif2m  3745  iinin2m  3746  unidif0  3941  mss  3981  eqvinop  3998  opcom  4005  opeqsn  4007  uniuni  4201  zfinf2  4330  elnn  4346  fconstmpt  4405  opeliunxp  4413  xpundi  4414  elvvv  4421  xpiindim  4491  elcnv2  4531  cnvuni  4539  dmuni  4563  opelres  4635  elima3  4695  imai  4701  imainss  4759  ssrnres  4783  cnvresima  4830  mptpreima  4834  coundir  4843  rnco  4847  coass  4859  relrelss  4864  dffun2  4932  dffun4  4933  dffun6f  4935  dffun4f  4938  dffun7  4948  dffun8  4949  dffun9  4950  svrelfun  4984  fncnv  4985  funcnvuni  4988  dfmpt3  5041  fintm  5095  fin  5096  dff12  5111  fores  5135  dff1o4  5154  eqfnfv3  5288  unpreima  5313  ffnfvf  5345  dff13f  5430  ffnov  5625  eqfnov  5627  foov  5667  opabex3d  5768  opabex3  5769  mpt2xopovel  5879  tpostpos  5902  dfsmo2  5925  erinxp  6203  xpassen  6327  distrnqg  6577  subhalfnqq  6604  enq0enq  6621  enq0sym  6622  enq0tr  6624  addnq0mo  6637  mulnq0mo  6638  distrnq0  6649  prarloc  6693  nqprrnd  6733  ltexprlemopl  6791  ltexprlemlol  6792  ltexprlemopu  6793  ltexprlemupu  6794  ltexprlemdisj  6796  ltexprlemloc  6797  recexprlemdisj  6820  caucvgprprlemell  6875  caucvgprprlemelu  6876  addsrmo  6920  mulsrmo  6921  opelreal  6996  axcaucvglemres  7065  elnnz  8361  elznn0nn  8365  zltlen  8426  suprzclex  8445  peano2uz2  8454  peano5uzti  8455  qltlen  8725  elfzuzb  9039  4fvwrd4  9150  fzind2  9248  cvg1nlemres  9871  rexfiuz  9875  ndvdssub  10330  isprm2  10499  isprm4  10501