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  2703  ceqsex3v  2781  rexab  2901  rexrab  2902  rmo4  2932  rmo3f  2936  reuind  2944  sbc3an  3026  rmo3  3056  ssrab  3235  rexun  3317  elin3  3328  inass  3347  unssdif  3372  indifdir  3393  difin2  3399  inrab2  3410  rabun2  3416  reuun2  3420  undif4  3487  rexdifpr  3622  rexsns  3633  rexdifsn  3726  2ralunsn  3800  iuncom4  3895  iunxiun  3970  inuni  4157  unidif0  4169  bnd2  4175  otth2  4243  copsexg  4246  copsex4g  4249  opeqsn  4254  opelopabsbALT  4261  elpwpwel  4477  suc11g  4558  rabxp  4665  opeliunxp  4683  xpundir  4685  xpiundi  4686  xpiundir  4687  brinxp2  4695  rexiunxp  4771  brres  4915  brresg  4917  dmres  4930  resiexg  4954  dminss  5045  imainss  5046  ssrnres  5073  elxp4  5118  elxp5  5119  cnvresima  5120  coundi  5132  resco  5135  imaco  5136  coiun  5140  coi1  5146  coass  5149  xpcom  5177  dffun2  5228  fncnv  5284  imadiflem  5297  imadif  5298  imainlem  5299  mptun  5349  fcnvres  5401  dff1o2  5468  dff1o3  5469  ffoss  5495  f11o  5496  brprcneu  5510  fvun2  5585  eqfnfv3  5617  respreima  5646  f1ompt  5669  fsn  5690  abrexco  5762  imaiun  5763  f1mpt  5774  dff1o6  5779  oprabid  5909  dfoprab2  5924  oprab4  5948  mpomptx  5968  opabex3d  6124  opabex3  6125  abexssex  6128  dfopab2  6192  dfoprab3s  6193  1stconst  6224  2ndconst  6225  xporderlem  6234  spc2ed  6236  f1od2  6238  brtpos2  6254  tpostpos  6267  tposmpo  6284  oviec  6643  mapsncnv  6697  dfixp  6702  domen  6753  mapsnen  6813  xpsnen  6823  xpcomco  6828  xpassen  6832  ltexpi  7338  dfmq0qs  7430  dfplq0qs  7431  enq0enq  7432  enq0ref  7434  enq0tr  7435  nqnq0pi  7439  prnmaxl  7489  prnminu  7490  suplocexprlemloc  7722  addsrpr  7746  mulsrpr  7747  suplocsrlemb  7807  addcnsr  7835  mulcnsr  7836  ltresr  7840  addvalex  7845  axprecex  7881  elnnz  9265  fnn0ind  9371  rexuz2  9583  qreccl  9644  rexrp  9678  elixx3g  9903  elfz2  10017  elfzuzb  10021  fznn  10091  elfz2nn0  10114  fznn0  10115  4fvwrd4  10142  elfzo2  10152  fzind2  10241  cvg1nlemres  10996  fsum2dlemstep  11444  modfsummod  11468  fprodseq  11593  divalgb  11932  bezoutlemmain  12001  isprm2  12119  oddpwdc  12176  prdsex  12723  xpscf  12771  issubg3  13057  releqgg  13085  ntreq0  13717  cnnei  13817  txlm  13864  blres  14019  isms2  14039  dedekindicclemicc  14195  limcrcl  14212  bdcriota  14720  bj-peano4  14792  alsconv  14913