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  590  pm5.53  802  pm5.75  962  3ancoma  985  3ioran  993  an6  1321  19.26-3an  1483  19.28h  1562  19.28  1563  eeeanv  1933  sb3an  1958  moanim  2100  nfrexdya  2513  r19.26-3  2607  r19.41  2632  rexcomf  2639  3reeanv  2648  cbvreu  2702  ceqsex3v  2780  rexab  2900  rexrab  2901  rmo4  2931  rmo3f  2935  reuind  2943  sbc3an  3025  rmo3  3055  ssrab  3234  rexun  3316  elin3  3327  inass  3346  unssdif  3371  indifdir  3392  difin2  3398  inrab2  3409  rabun2  3415  reuun2  3419  undif4  3486  rexdifpr  3621  rexsns  3632  rexdifsn  3725  2ralunsn  3799  iuncom4  3894  iunxiun  3969  inuni  4156  unidif0  4168  bnd2  4174  otth2  4242  copsexg  4245  copsex4g  4248  opeqsn  4253  opelopabsbALT  4260  elpwpwel  4476  suc11g  4557  rabxp  4664  opeliunxp  4682  xpundir  4684  xpiundi  4685  xpiundir  4686  brinxp2  4694  rexiunxp  4770  brres  4914  brresg  4916  dmres  4929  resiexg  4953  dminss  5044  imainss  5045  ssrnres  5072  elxp4  5117  elxp5  5118  cnvresima  5119  coundi  5131  resco  5134  imaco  5135  coiun  5139  coi1  5145  coass  5148  xpcom  5176  dffun2  5227  fncnv  5283  imadiflem  5296  imadif  5297  imainlem  5298  mptun  5348  fcnvres  5400  dff1o2  5467  dff1o3  5468  ffoss  5494  f11o  5495  brprcneu  5509  fvun2  5584  eqfnfv3  5616  respreima  5645  f1ompt  5668  fsn  5689  abrexco  5760  imaiun  5761  f1mpt  5772  dff1o6  5777  oprabid  5907  dfoprab2  5922  oprab4  5946  mpomptx  5966  opabex3d  6122  opabex3  6123  abexssex  6126  dfopab2  6190  dfoprab3s  6191  1stconst  6222  2ndconst  6223  xporderlem  6232  spc2ed  6234  f1od2  6236  brtpos2  6252  tpostpos  6265  tposmpo  6282  oviec  6641  mapsncnv  6695  dfixp  6700  domen  6751  mapsnen  6811  xpsnen  6821  xpcomco  6826  xpassen  6830  ltexpi  7336  dfmq0qs  7428  dfplq0qs  7429  enq0enq  7430  enq0ref  7432  enq0tr  7433  nqnq0pi  7437  prnmaxl  7487  prnminu  7488  suplocexprlemloc  7720  addsrpr  7744  mulsrpr  7745  suplocsrlemb  7805  addcnsr  7833  mulcnsr  7834  ltresr  7838  addvalex  7843  axprecex  7879  elnnz  9263  fnn0ind  9369  rexuz2  9581  qreccl  9642  rexrp  9676  elixx3g  9901  elfz2  10015  elfzuzb  10019  fznn  10089  elfz2nn0  10112  fznn0  10113  4fvwrd4  10140  elfzo2  10150  fzind2  10239  cvg1nlemres  10994  fsum2dlemstep  11442  modfsummod  11466  fprodseq  11591  divalgb  11930  bezoutlemmain  11999  isprm2  12117  oddpwdc  12174  prdsex  12718  xpscf  12766  issubg3  13052  releqgg  13080  ntreq0  13635  cnnei  13735  txlm  13782  blres  13937  isms2  13957  dedekindicclemicc  14113  limcrcl  14130  bdcriota  14638  bj-peano4  14710  alsconv  14830