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  804  pm5.75  965  3ancoma  988  3ioran  996  an6  1334  19.26-3an  1507  19.28h  1586  19.28  1587  eeeanv  1962  sb3an  1987  moanim  2130  nfrexdya  2544  r19.26-3  2638  r19.41  2663  rexcomf  2670  3reeanv  2679  cbvreu  2740  ceqsex3v  2820  rexab  2942  rexrab  2943  rmo4  2973  rmo3f  2977  reuind  2985  sbc3an  3067  rmo3  3098  ssrab  3279  rexun  3361  elin3  3372  inass  3391  unssdif  3416  indifdir  3437  difin2  3443  inrab2  3454  rabun2  3460  reuun2  3464  undif4  3531  rexdifpr  3671  rexsns  3682  rexdifsn  3776  2ralunsn  3853  iuncom4  3948  iunxiun  4023  inuni  4215  unidif0  4227  bnd2  4233  otth2  4303  copsexg  4306  copsex4g  4309  opeqsn  4315  opelopabsbALT  4323  elpwpwel  4540  suc11g  4623  rabxp  4730  opeliunxp  4748  xpundir  4750  xpiundi  4751  xpiundir  4752  brinxp2  4760  rexiunxp  4838  brres  4984  brresg  4986  dmres  4999  resiexg  5023  dminss  5116  imainss  5117  ssrnres  5144  elxp4  5189  elxp5  5190  cnvresima  5191  coundi  5203  resco  5206  imaco  5207  coiun  5211  coi1  5217  coass  5220  xpcom  5248  dffun2  5300  fncnv  5359  imadiflem  5372  imadif  5373  imainlem  5374  mptun  5427  fcnvres  5481  dff1o2  5549  dff1o3  5550  ffoss  5576  f11o  5577  brprcneu  5592  fvun2  5669  eqfnfv3  5702  respreima  5731  f1ompt  5754  fsn  5775  abrexco  5851  imaiun  5852  f1mpt  5863  dff1o6  5868  oprabid  5999  dfoprab2  6015  oprab4  6039  mpomptx  6059  opabex3d  6229  opabex3  6230  abexssex  6233  dfopab2  6298  dfoprab3s  6299  1stconst  6330  2ndconst  6331  xporderlem  6340  spc2ed  6342  f1od2  6344  brtpos2  6360  tpostpos  6373  tposmpo  6390  oviec  6751  mapsncnv  6805  dfixp  6810  domen  6863  mapsnen  6927  xpsnen  6941  xpcomco  6946  xpassen  6950  ltexpi  7485  dfmq0qs  7577  dfplq0qs  7578  enq0enq  7579  enq0ref  7581  enq0tr  7582  nqnq0pi  7586  prnmaxl  7636  prnminu  7637  suplocexprlemloc  7869  addsrpr  7893  mulsrpr  7894  suplocsrlemb  7954  addcnsr  7982  mulcnsr  7983  ltresr  7987  addvalex  7992  axprecex  8028  elnnz  9417  fnn0ind  9524  rexuz2  9737  qreccl  9798  rexrp  9833  elixx3g  10058  elfz2  10172  elfzuzb  10176  fznn  10246  elfz2nn0  10269  fznn0  10270  4fvwrd4  10297  elfzo2  10307  fzind2  10405  cvg1nlemres  11411  fsum2dlemstep  11860  modfsummod  11884  fprodseq  12009  divalgb  12351  bezoutlemmain  12434  isprm2  12554  oddpwdc  12611  prdsex  13216  prdsval  13220  prdsbaslemss  13221  xpscf  13294  issubg3  13643  releqgg  13671  eqgex  13672  imasabl  13787  dfrhm2  14031  ntreq0  14719  cnnei  14819  txlm  14866  blres  15021  isms2  15041  dedekindicclemicc  15219  limcrcl  15245  lgsquadlem1  15669  lgsquadlem2  15670  bdcriota  16018  bj-peano4  16090  alsconv  16221