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  809  pm5.75  970  3ancoma  1011  3ioran  1019  an6  1357  19.26-3an  1531  19.28h  1610  19.28  1611  eeeanv  1986  sb3an  2011  moanim  2154  nfrexdya  2568  r19.26-3  2663  r19.41  2688  rexcomf  2695  3reeanv  2704  cbvreu  2765  ceqsex3v  2846  rexab  2968  rexrab  2969  rmo4  2999  rmo3f  3003  reuind  3011  sbc3an  3093  rmo3  3124  ssrab  3305  rexun  3387  elin3  3398  inass  3417  unssdif  3442  indifdir  3463  difin2  3469  inrab2  3480  rabun2  3486  reuun2  3490  undif4  3557  rexdifpr  3697  rexsns  3708  rexdifsn  3805  2ralunsn  3882  iuncom4  3977  iunxiun  4052  inuni  4245  unidif0  4257  bnd2  4263  otth2  4333  copsexg  4336  copsex4g  4339  opeqsn  4345  opelopabsbALT  4353  elpwpwel  4572  suc11g  4655  rabxp  4763  opeliunxp  4781  xpundir  4783  xpiundi  4784  xpiundir  4785  brinxp2  4793  rexiunxp  4872  brres  5019  brresg  5021  dmres  5034  resiexg  5058  dminss  5151  imainss  5152  ssrnres  5179  elxp4  5224  elxp5  5225  cnvresima  5226  coundi  5238  resco  5241  imaco  5242  coiun  5246  coi1  5252  coass  5255  xpcom  5283  dffun2  5336  fncnv  5396  imadiflem  5409  imadif  5410  imainlem  5411  mptun  5464  fcnvres  5520  dff1o2  5588  dff1o3  5589  ffoss  5616  f11o  5617  brprcneu  5632  fvun2  5713  eqfnfv3  5746  respreima  5775  f1ompt  5798  fsn  5819  abrexco  5900  imaiun  5901  f1mpt  5912  dff1o6  5917  oprabid  6050  dfoprab2  6068  oprab4  6092  mpomptx  6112  opabex3d  6283  opabex3  6284  abexssex  6287  dfopab2  6352  dfoprab3s  6353  1stconst  6386  2ndconst  6387  xporderlem  6396  spc2ed  6398  f1od2  6400  brtpos2  6417  tpostpos  6430  tposmpo  6447  oviec  6810  mapsncnv  6864  dfixp  6869  domen  6922  mapsnen  6986  xpsnen  7005  xpcomco  7010  xpassen  7014  sspw1or2  7403  ltexpi  7557  dfmq0qs  7649  dfplq0qs  7650  enq0enq  7651  enq0ref  7653  enq0tr  7654  nqnq0pi  7658  prnmaxl  7708  prnminu  7709  suplocexprlemloc  7941  addsrpr  7965  mulsrpr  7966  suplocsrlemb  8026  addcnsr  8054  mulcnsr  8055  ltresr  8059  addvalex  8064  axprecex  8100  elnnz  9489  fnn0ind  9596  rexuz2  9815  qreccl  9876  rexrp  9911  elixx3g  10136  elfz2  10250  elfzuzb  10254  fznn  10324  elfz2nn0  10347  fznn0  10348  4fvwrd4  10375  elfzo2  10385  fzind2  10486  cvg1nlemres  11563  fsum2dlemstep  12013  modfsummod  12037  fprodseq  12162  divalgb  12504  bezoutlemmain  12587  isprm2  12707  oddpwdc  12764  prdsex  13370  prdsval  13374  prdsbaslemss  13375  xpscf  13448  issubg3  13797  releqgg  13825  eqgex  13826  imasabl  13941  dfrhm2  14187  ntreq0  14875  cnnei  14975  txlm  15022  blres  15177  isms2  15197  dedekindicclemicc  15375  limcrcl  15401  lgsquadlem1  15825  lgsquadlem2  15826  isclwwlknx  16286  clwwlknonel  16302  clwwlknon2x  16305  iseupthf1o  16318  bdcriota  16529  bj-peano4  16601  alsconv  16746