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  1986  sb3an  2011  moanim  2154  nfrexdya  2569  r19.26-3  2664  r19.41  2689  rexcomf  2696  3reeanv  2705  cbvreu  2766  ceqsex3v  2847  rexab  2969  rexrab  2970  rmo4  3000  rmo3f  3004  reuind  3012  sbc3an  3094  rmo3  3125  ssrab  3306  rexun  3389  elin3  3400  inass  3419  unssdif  3444  indifdir  3465  difin2  3471  inrab2  3482  rabun2  3488  reuun2  3492  undif4  3559  rexdifpr  3701  rexsns  3712  rexdifsn  3809  2ralunsn  3887  iuncom4  3982  iunxiun  4057  inuni  4250  unidif0  4263  bnd2  4269  otth2  4339  copsexg  4342  copsex4g  4345  opeqsn  4351  opelopabsbALT  4359  elpwpwel  4578  suc11g  4661  rabxp  4769  opeliunxp  4787  xpundir  4789  xpiundi  4790  xpiundir  4791  brinxp2  4799  rexiunxp  4878  brres  5025  brresg  5027  dmres  5040  resiexg  5064  dminss  5158  imainss  5159  ssrnres  5186  elxp4  5231  elxp5  5232  cnvresima  5233  coundi  5245  resco  5248  imaco  5249  coiun  5253  coi1  5259  coass  5262  xpcom  5290  dffun2  5343  fncnv  5403  imadiflem  5416  imadif  5417  imainlem  5418  mptun  5471  fcnvres  5528  dff1o2  5597  dff1o3  5598  ffoss  5625  f11o  5626  brprcneu  5641  fvun2  5722  eqfnfv3  5755  respreima  5783  f1ompt  5806  fsn  5827  abrexco  5910  imaiun  5911  f1mpt  5922  dff1o6  5927  oprabid  6060  dfoprab2  6078  oprab4  6102  mpomptx  6122  opabex3d  6292  opabex3  6293  abexssex  6296  dfopab2  6361  dfoprab3s  6362  1stconst  6395  2ndconst  6396  xporderlem  6405  spc2ed  6407  f1od2  6409  brtpos2  6460  tpostpos  6473  tposmpo  6490  oviec  6853  mapsncnv  6907  dfixp  6912  domen  6965  mapsnen  7029  xpsnen  7048  xpcomco  7053  xpassen  7057  sspw1or2  7463  ltexpi  7617  dfmq0qs  7709  dfplq0qs  7710  enq0enq  7711  enq0ref  7713  enq0tr  7714  nqnq0pi  7718  prnmaxl  7768  prnminu  7769  suplocexprlemloc  8001  addsrpr  8025  mulsrpr  8026  suplocsrlemb  8086  addcnsr  8114  mulcnsr  8115  ltresr  8119  addvalex  8124  axprecex  8160  elnnz  9550  fnn0ind  9657  rexuz2  9876  qreccl  9937  rexrp  9972  elixx3g  10197  elfz2  10312  elfzuzb  10316  fznn  10386  elfz2nn0  10409  fznn0  10410  4fvwrd4  10437  elfzo2  10447  fzind2  10548  cvg1nlemres  11625  fsum2dlemstep  12075  modfsummod  12099  fprodseq  12224  divalgb  12566  bezoutlemmain  12649  isprm2  12769  oddpwdc  12826  prdsex  13432  prdsval  13436  prdsbaslemss  13437  xpscf  13510  issubg3  13859  releqgg  13887  eqgex  13888  imasabl  14003  dfrhm2  14249  ntreq0  14943  cnnei  15043  txlm  15090  blres  15245  isms2  15265  dedekindicclemicc  15443  limcrcl  15469  lgsquadlem1  15896  lgsquadlem2  15897  isclwwlknx  16357  clwwlknonel  16373  clwwlknon2x  16376  iseupthf1o  16389  bdcriota  16599  bj-peano4  16671  alsconv  16823