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  592  pm5.53  807  pm5.75  968  3ancoma  1009  3ioran  1017  an6  1355  19.26-3an  1529  19.28h  1608  19.28  1609  eeeanv  1984  sb3an  2009  moanim  2152  nfrexdya  2566  r19.26-3  2661  r19.41  2686  rexcomf  2693  3reeanv  2702  cbvreu  2763  ceqsex3v  2843  rexab  2965  rexrab  2966  rmo4  2996  rmo3f  3000  reuind  3008  sbc3an  3090  rmo3  3121  ssrab  3302  rexun  3384  elin3  3395  inass  3414  unssdif  3439  indifdir  3460  difin2  3466  inrab2  3477  rabun2  3483  reuun2  3487  undif4  3554  rexdifpr  3694  rexsns  3705  rexdifsn  3800  2ralunsn  3877  iuncom4  3972  iunxiun  4047  inuni  4239  unidif0  4251  bnd2  4257  otth2  4327  copsexg  4330  copsex4g  4333  opeqsn  4339  opelopabsbALT  4347  elpwpwel  4566  suc11g  4649  rabxp  4756  opeliunxp  4774  xpundir  4776  xpiundi  4777  xpiundir  4778  brinxp2  4786  rexiunxp  4864  brres  5011  brresg  5013  dmres  5026  resiexg  5050  dminss  5143  imainss  5144  ssrnres  5171  elxp4  5216  elxp5  5217  cnvresima  5218  coundi  5230  resco  5233  imaco  5234  coiun  5238  coi1  5244  coass  5247  xpcom  5275  dffun2  5328  fncnv  5387  imadiflem  5400  imadif  5401  imainlem  5402  mptun  5455  fcnvres  5509  dff1o2  5577  dff1o3  5578  ffoss  5604  f11o  5605  brprcneu  5620  fvun2  5701  eqfnfv3  5734  respreima  5763  f1ompt  5786  fsn  5807  abrexco  5883  imaiun  5884  f1mpt  5895  dff1o6  5900  oprabid  6033  dfoprab2  6051  oprab4  6075  mpomptx  6095  opabex3d  6266  opabex3  6267  abexssex  6270  dfopab2  6335  dfoprab3s  6336  1stconst  6367  2ndconst  6368  xporderlem  6377  spc2ed  6379  f1od2  6381  brtpos2  6397  tpostpos  6410  tposmpo  6427  oviec  6788  mapsncnv  6842  dfixp  6847  domen  6900  mapsnen  6964  xpsnen  6980  xpcomco  6985  xpassen  6989  ltexpi  7524  dfmq0qs  7616  dfplq0qs  7617  enq0enq  7618  enq0ref  7620  enq0tr  7621  nqnq0pi  7625  prnmaxl  7675  prnminu  7676  suplocexprlemloc  7908  addsrpr  7932  mulsrpr  7933  suplocsrlemb  7993  addcnsr  8021  mulcnsr  8022  ltresr  8026  addvalex  8031  axprecex  8067  elnnz  9456  fnn0ind  9563  rexuz2  9776  qreccl  9837  rexrp  9872  elixx3g  10097  elfz2  10211  elfzuzb  10215  fznn  10285  elfz2nn0  10308  fznn0  10309  4fvwrd4  10336  elfzo2  10346  fzind2  10445  cvg1nlemres  11496  fsum2dlemstep  11945  modfsummod  11969  fprodseq  12094  divalgb  12436  bezoutlemmain  12519  isprm2  12639  oddpwdc  12696  prdsex  13302  prdsval  13306  prdsbaslemss  13307  xpscf  13380  issubg3  13729  releqgg  13757  eqgex  13758  imasabl  13873  dfrhm2  14118  ntreq0  14806  cnnei  14906  txlm  14953  blres  15108  isms2  15128  dedekindicclemicc  15306  limcrcl  15332  lgsquadlem1  15756  lgsquadlem2  15757  bdcriota  16246  bj-peano4  16318  alsconv  16448