Theorem anbi1i 458

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

Hypothesis

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

Assertion

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

Proof of Theorem anbi1i

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

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:  anbi2ci  459  anbi12i  460  bianassc  470  an12  561  anandi  590  pm5.53  803  pm5.75  964  3ancoma  987  3ioran  995  an6  1332  19.26-3an  1494  19.28h  1573  19.28  1574  eeeanv  1949  sb3an  1974  moanim  2116  nfrexdya  2530  r19.26-3  2624  r19.41  2649  rexcomf  2656  3reeanv  2665  cbvreu  2724  ceqsex3v  2803  rexab  2923  rexrab  2924  rmo4  2954  rmo3f  2958  reuind  2966  sbc3an  3048  rmo3  3078  ssrab  3258  rexun  3340  elin3  3351  inass  3370  unssdif  3395  indifdir  3416  difin2  3422  inrab2  3433  rabun2  3439  reuun2  3443  undif4  3510  rexdifpr  3647  rexsns  3658  rexdifsn  3751  2ralunsn  3825  iuncom4  3920  iunxiun  3995  inuni  4185  unidif0  4197  bnd2  4203  otth2  4271  copsexg  4274  copsex4g  4277  opeqsn  4282  opelopabsbALT  4290  elpwpwel  4507  suc11g  4590  rabxp  4697  opeliunxp  4715  xpundir  4717  xpiundi  4718  xpiundir  4719  brinxp2  4727  rexiunxp  4805  brres  4949  brresg  4951  dmres  4964  resiexg  4988  dminss  5081  imainss  5082  ssrnres  5109  elxp4  5154  elxp5  5155  cnvresima  5156  coundi  5168  resco  5171  imaco  5172  coiun  5176  coi1  5182  coass  5185  xpcom  5213  dffun2  5265  fncnv  5321  imadiflem  5334  imadif  5335  imainlem  5336  mptun  5386  fcnvres  5438  dff1o2  5506  dff1o3  5507  ffoss  5533  f11o  5534  brprcneu  5548  fvun2  5625  eqfnfv3  5658  respreima  5687  f1ompt  5710  fsn  5731  abrexco  5803  imaiun  5804  f1mpt  5815  dff1o6  5820  oprabid  5951  dfoprab2  5966  oprab4  5990  mpomptx  6010  opabex3d  6175  opabex3  6176  abexssex  6179  dfopab2  6244  dfoprab3s  6245  1stconst  6276  2ndconst  6277  xporderlem  6286  spc2ed  6288  f1od2  6290  brtpos2  6306  tpostpos  6319  tposmpo  6336  oviec  6697  mapsncnv  6751  dfixp  6756  domen  6807  mapsnen  6867  xpsnen  6877  xpcomco  6882  xpassen  6886  ltexpi  7399  dfmq0qs  7491  dfplq0qs  7492  enq0enq  7493  enq0ref  7495  enq0tr  7496  nqnq0pi  7500  prnmaxl  7550  prnminu  7551  suplocexprlemloc  7783  addsrpr  7807  mulsrpr  7808  suplocsrlemb  7868  addcnsr  7896  mulcnsr  7897  ltresr  7901  addvalex  7906  axprecex  7942  elnnz  9330  fnn0ind  9436  rexuz2  9649  qreccl  9710  rexrp  9745  elixx3g  9970  elfz2  10084  elfzuzb  10088  fznn  10158  elfz2nn0  10181  fznn0  10182  4fvwrd4  10209  elfzo2  10219  fzind2  10309  cvg1nlemres  11132  fsum2dlemstep  11580  modfsummod  11604  fprodseq  11729  divalgb  12069  bezoutlemmain  12138  isprm2  12258  oddpwdc  12315  prdsex  12883  xpscf  12933  issubg3  13265  releqgg  13293  eqgex  13294  imasabl  13409  dfrhm2  13653  ntreq0  14311  cnnei  14411  txlm  14458  blres  14613  isms2  14633  dedekindicclemicc  14811  limcrcl  14837  lgsquadlem1  15234  lgsquadlem2  15235  bdcriota  15445  bj-peano4  15517  alsconv  15640