Theorem anbi1i 454

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 451	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  455  anbi12i  456  an12  551  anandi  580  pm5.53  792  pm5.75  947  3ancoma  970  3ioran  978  an6  1303  19.26-3an  1463  19.28h  1542  19.28  1543  eeeanv  1913  sb3an  1938  moanim  2080  nfrexdya  2493  r19.26-3  2587  r19.41  2612  rexcomf  2619  3reeanv  2627  cbvreu  2678  ceqsex3v  2754  rexab  2874  rexrab  2875  rmo4  2905  rmo3f  2909  reuind  2917  sbc3an  2998  rmo3  3028  ssrab  3206  rexun  3287  elin3  3298  inass  3317  unssdif  3342  indifdir  3363  difin2  3369  inrab2  3380  rabun2  3386  reuun2  3390  undif4  3456  rexdifpr  3588  rexsns  3599  rexdifsn  3692  2ralunsn  3762  iuncom4  3857  iunxiun  3931  inuni  4117  unidif0  4129  bnd2  4135  otth2  4202  copsexg  4205  copsex4g  4208  opeqsn  4213  opelopabsbALT  4220  elpwpwel  4436  suc11g  4517  rabxp  4624  opeliunxp  4642  xpundir  4644  xpiundi  4645  xpiundir  4646  brinxp2  4654  rexiunxp  4729  brres  4873  brresg  4875  dmres  4888  resiexg  4912  dminss  5001  imainss  5002  ssrnres  5029  elxp4  5074  elxp5  5075  cnvresima  5076  coundi  5088  resco  5091  imaco  5092  coiun  5096  coi1  5102  coass  5105  xpcom  5133  dffun2  5181  fncnv  5237  imadiflem  5250  imadif  5251  imainlem  5252  mptun  5302  fcnvres  5354  dff1o2  5420  dff1o3  5421  ffoss  5447  f11o  5448  brprcneu  5462  fvun2  5536  eqfnfv3  5568  respreima  5596  f1ompt  5619  fsn  5640  abrexco  5710  imaiun  5711  f1mpt  5722  dff1o6  5727  oprabid  5854  dfoprab2  5869  oprab4  5893  mpomptx  5913  opabex3d  6070  opabex3  6071  abexssex  6074  dfopab2  6138  dfoprab3s  6139  1stconst  6169  2ndconst  6170  xporderlem  6179  spc2ed  6181  f1od2  6183  brtpos2  6199  tpostpos  6212  tposmpo  6229  oviec  6587  mapsncnv  6641  dfixp  6646  domen  6697  mapsnen  6757  xpsnen  6767  xpcomco  6772  xpassen  6776  ltexpi  7258  dfmq0qs  7350  dfplq0qs  7351  enq0enq  7352  enq0ref  7354  enq0tr  7355  nqnq0pi  7359  prnmaxl  7409  prnminu  7410  suplocexprlemloc  7642  addsrpr  7666  mulsrpr  7667  suplocsrlemb  7727  addcnsr  7755  mulcnsr  7756  ltresr  7760  addvalex  7765  axprecex  7801  elnnz  9178  fnn0ind  9281  rexuz2  9493  qreccl  9552  rexrp  9584  elixx3g  9806  elfz2  9920  elfzuzb  9923  fznn  9992  elfz2nn0  10015  fznn0  10016  4fvwrd4  10043  elfzo2  10053  fzind2  10142  cvg1nlemres  10889  fsum2dlemstep  11335  modfsummod  11359  fprodseq  11484  divalgb  11820  bezoutlemmain  11886  isprm2  11998  oddpwdc  12053  ntreq0  12574  cnnei  12674  txlm  12721  blres  12876  isms2  12896  dedekindicclemicc  13052  limcrcl  13069  bdcriota  13500  bj-peano4  13572  alsconv  13690