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  563  anandi  594  pm5.53  810  pm5.75  971  3ancoma  1012  3ioran  1020  an6  1358  19.26-3an  1532  19.28h  1611  19.28  1612  eeeanv  1989  sb3an  2014  moanim  2157  nfrexdya  2580  r19.26-3  2675  r19.41  2700  rexcomf  2707  3reeanv  2716  cbvreu  2778  ceqsex3v  2859  rexab  2982  rexrab  2983  rmo4  3013  rmo3f  3017  reuind  3025  sbc3an  3107  rmo3  3138  ssrab  3320  rexun  3403  elin3  3414  inass  3435  unssdif  3460  indifdir  3481  difin2  3487  inrab2  3498  rabun2  3504  reuun2  3508  undif4  3576  rexdifpr  3723  rexsns  3734  rexdifsn  3831  2ralunsn  3909  iuncom4  4004  iunxiun  4079  inuni  4273  unidif0  4286  bnd2  4292  otth2  4363  copsexg  4366  copsex4g  4369  opeqsn  4375  opelopabsbALT  4383  elpwpwel  4603  suc11g  4686  rabxp  4794  opeliunxp  4812  xpundir  4814  xpiundi  4815  xpiundir  4816  brinxp2  4824  rexiunxp  4904  brres  5051  brresg  5053  dmres  5066  resiexg  5090  dminss  5184  imainss  5185  ssrnres  5212  elxp4  5257  elxp5  5258  cnvresima  5259  coundi  5271  resco  5274  imaco  5275  coiun  5279  coi1  5285  coass  5288  xpcom  5316  dffun2  5369  fncnv  5429  imadiflem  5442  imadif  5443  imainlem  5444  mptun  5497  fcnvres  5557  dff1o2  5626  dff1o3  5627  ffoss  5654  f11o  5655  brprcneu  5670  fvun2  5751  eqfnfv3  5784  respreima  5812  f1ompt  5835  fsn  5856  abrexco  5940  imaiun  5941  f1mpt  5952  dff1o6  5957  oprabid  6092  dfoprab2  6110  oprab4  6134  mpomptx  6154  opabex3d  6325  opabex3  6326  abexssex  6329  dfopab2  6398  dfoprab3s  6399  1stconst  6432  2ndconst  6433  xporderlem  6442  spc2ed  6444  f1od2  6446  brtpos2  6497  tpostpos  6510  tposmpo  6527  oviec  6890  mapsncnv  6945  dfixp  6950  domen  7003  mapsnen  7068  xpsnen  7087  xpcomco  7092  xpassen  7096  sspw1or2  7510  ltexpi  7670  dfmq0qs  7762  dfplq0qs  7763  enq0enq  7764  enq0ref  7766  enq0tr  7767  nqnq0pi  7771  prnmaxl  7821  prnminu  7822  suplocexprlemloc  8054  addsrpr  8078  mulsrpr  8079  suplocsrlemb  8139  addcnsr  8167  mulcnsr  8168  ltresr  8172  addvalex  8177  axprecex  8213  elnnz  9609  fnn0ind  9717  rexuz2  9936  qreccl  9997  rexrp  10032  elixx3g  10258  elfz2  10373  elfzuzb  10377  fznn  10450  elfz2nn0  10473  fznn0  10474  4fvwrd4  10501  elfzo2  10511  fzind2  10612  sseqn  11233  cvg1nlemres  11701  fsum2dlemstep  12151  modfsummod  12175  fprodseq  12300  divalgb  12642  bezoutlemmain  12725  isprm2  12845  oddpwdc  12902  ballotfilemelo  13172  ballotfilem2  13178  ballotfilemfc0  13182  ballotfilemfcc  13183  xpscf  13617  issubg3  13951  releqgg  13979  eqgex  13980  imasabl  14095  prdsex  14120  prdsval  14121  prdsbaslemss  14122  dfrhm2  14405  drngprop  14561  ntreq0  15129  cnnei  15229  txlm  15276  blres  15431  isms2  15451  dedekindicclemicc  15629  limcrcl  15655  lgsquadlem1  16082  lgsquadlem2  16083  isclwwlknx  16543  clwwlknonel  16559  clwwlknon2x  16562  iseupthf1o  16575  bdcriota  16795  bj-peano4  16867  alsconv  17007