Theorem anbi1i 454

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

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:  anbi2ci  455  anbi12i  456  an12  551  anandi  580  pm5.53  792  pm5.75  952  3ancoma  975  3ioran  983  an6  1311  19.26-3an  1471  19.28h  1550  19.28  1551  eeeanv  1921  sb3an  1946  moanim  2088  nfrexdya  2502  r19.26-3  2596  r19.41  2621  rexcomf  2628  3reeanv  2636  cbvreu  2690  ceqsex3v  2768  rexab  2888  rexrab  2889  rmo4  2919  rmo3f  2923  reuind  2931  sbc3an  3012  rmo3  3042  ssrab  3220  rexun  3302  elin3  3313  inass  3332  unssdif  3357  indifdir  3378  difin2  3384  inrab2  3395  rabun2  3401  reuun2  3405  undif4  3471  rexdifpr  3604  rexsns  3615  rexdifsn  3708  2ralunsn  3778  iuncom4  3873  iunxiun  3947  inuni  4134  unidif0  4146  bnd2  4152  otth2  4219  copsexg  4222  copsex4g  4225  opeqsn  4230  opelopabsbALT  4237  elpwpwel  4453  suc11g  4534  rabxp  4641  opeliunxp  4659  xpundir  4661  xpiundi  4662  xpiundir  4663  brinxp2  4671  rexiunxp  4746  brres  4890  brresg  4892  dmres  4905  resiexg  4929  dminss  5018  imainss  5019  ssrnres  5046  elxp4  5091  elxp5  5092  cnvresima  5093  coundi  5105  resco  5108  imaco  5109  coiun  5113  coi1  5119  coass  5122  xpcom  5150  dffun2  5198  fncnv  5254  imadiflem  5267  imadif  5268  imainlem  5269  mptun  5319  fcnvres  5371  dff1o2  5437  dff1o3  5438  ffoss  5464  f11o  5465  brprcneu  5479  fvun2  5553  eqfnfv3  5585  respreima  5613  f1ompt  5636  fsn  5657  abrexco  5727  imaiun  5728  f1mpt  5739  dff1o6  5744  oprabid  5874  dfoprab2  5889  oprab4  5913  mpomptx  5933  opabex3d  6089  opabex3  6090  abexssex  6093  dfopab2  6157  dfoprab3s  6158  1stconst  6189  2ndconst  6190  xporderlem  6199  spc2ed  6201  f1od2  6203  brtpos2  6219  tpostpos  6232  tposmpo  6249  oviec  6607  mapsncnv  6661  dfixp  6666  domen  6717  mapsnen  6777  xpsnen  6787  xpcomco  6792  xpassen  6796  ltexpi  7278  dfmq0qs  7370  dfplq0qs  7371  enq0enq  7372  enq0ref  7374  enq0tr  7375  nqnq0pi  7379  prnmaxl  7429  prnminu  7430  suplocexprlemloc  7662  addsrpr  7686  mulsrpr  7687  suplocsrlemb  7747  addcnsr  7775  mulcnsr  7776  ltresr  7780  addvalex  7785  axprecex  7821  elnnz  9201  fnn0ind  9307  rexuz2  9519  qreccl  9580  rexrp  9612  elixx3g  9837  elfz2  9951  elfzuzb  9954  fznn  10024  elfz2nn0  10047  fznn0  10048  4fvwrd4  10075  elfzo2  10085  fzind2  10174  cvg1nlemres  10927  fsum2dlemstep  11375  modfsummod  11399  fprodseq  11524  divalgb  11862  bezoutlemmain  11931  isprm2  12049  oddpwdc  12106  ntreq0  12772  cnnei  12872  txlm  12919  blres  13074  isms2  13094  dedekindicclemicc  13250  limcrcl  13267  bdcriota  13765  bj-peano4  13837  alsconv  13956