Theorem anbi1i 455

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 452	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  456  anbi12i  457  bianassc  467  an12  556  anandi  585  pm5.53  797  pm5.75  957  3ancoma  980  3ioran  988  an6  1316  19.26-3an  1476  19.28h  1555  19.28  1556  eeeanv  1926  sb3an  1951  moanim  2093  nfrexdya  2506  r19.26-3  2600  r19.41  2625  rexcomf  2632  3reeanv  2640  cbvreu  2694  ceqsex3v  2772  rexab  2892  rexrab  2893  rmo4  2923  rmo3f  2927  reuind  2935  sbc3an  3016  rmo3  3046  ssrab  3225  rexun  3307  elin3  3318  inass  3337  unssdif  3362  indifdir  3383  difin2  3389  inrab2  3400  rabun2  3406  reuun2  3410  undif4  3477  rexdifpr  3611  rexsns  3622  rexdifsn  3715  2ralunsn  3785  iuncom4  3880  iunxiun  3954  inuni  4141  unidif0  4153  bnd2  4159  otth2  4226  copsexg  4229  copsex4g  4232  opeqsn  4237  opelopabsbALT  4244  elpwpwel  4460  suc11g  4541  rabxp  4648  opeliunxp  4666  xpundir  4668  xpiundi  4669  xpiundir  4670  brinxp2  4678  rexiunxp  4753  brres  4897  brresg  4899  dmres  4912  resiexg  4936  dminss  5025  imainss  5026  ssrnres  5053  elxp4  5098  elxp5  5099  cnvresima  5100  coundi  5112  resco  5115  imaco  5116  coiun  5120  coi1  5126  coass  5129  xpcom  5157  dffun2  5208  fncnv  5264  imadiflem  5277  imadif  5278  imainlem  5279  mptun  5329  fcnvres  5381  dff1o2  5447  dff1o3  5448  ffoss  5474  f11o  5475  brprcneu  5489  fvun2  5563  eqfnfv3  5595  respreima  5624  f1ompt  5647  fsn  5668  abrexco  5738  imaiun  5739  f1mpt  5750  dff1o6  5755  oprabid  5885  dfoprab2  5900  oprab4  5924  mpomptx  5944  opabex3d  6100  opabex3  6101  abexssex  6104  dfopab2  6168  dfoprab3s  6169  1stconst  6200  2ndconst  6201  xporderlem  6210  spc2ed  6212  f1od2  6214  brtpos2  6230  tpostpos  6243  tposmpo  6260  oviec  6619  mapsncnv  6673  dfixp  6678  domen  6729  mapsnen  6789  xpsnen  6799  xpcomco  6804  xpassen  6808  ltexpi  7299  dfmq0qs  7391  dfplq0qs  7392  enq0enq  7393  enq0ref  7395  enq0tr  7396  nqnq0pi  7400  prnmaxl  7450  prnminu  7451  suplocexprlemloc  7683  addsrpr  7707  mulsrpr  7708  suplocsrlemb  7768  addcnsr  7796  mulcnsr  7797  ltresr  7801  addvalex  7806  axprecex  7842  elnnz  9222  fnn0ind  9328  rexuz2  9540  qreccl  9601  rexrp  9633  elixx3g  9858  elfz2  9972  elfzuzb  9975  fznn  10045  elfz2nn0  10068  fznn0  10069  4fvwrd4  10096  elfzo2  10106  fzind2  10195  cvg1nlemres  10949  fsum2dlemstep  11397  modfsummod  11421  fprodseq  11546  divalgb  11884  bezoutlemmain  11953  isprm2  12071  oddpwdc  12128  ntreq0  12926  cnnei  13026  txlm  13073  blres  13228  isms2  13248  dedekindicclemicc  13404  limcrcl  13421  bdcriota  13918  bj-peano4  13990  alsconv  14109