Theorem anbi1i 431

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 428	1 |- ( ( ph /\ ch ) <-> ( ps /\ ch ) )

Syntax hints:   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  anbi2ci  432  anbi12i  433  an12  495  anandi  524  pm5.53  715  pm5.75  869  3ancoma  892  3ioran  900  an6  1216  19.26-3an  1372  19.28h  1454  19.28  1455  eeeanv  1808  sb3an  1832  moanim  1974  nfrexdya  2359  r19.26-3  2443  r19.41  2465  rexcomf  2472  3reeanv  2480  cbvreu  2531  ceqsex3v  2596  rexab  2703  rexrab  2704  rmo4  2734  reuind  2744  rmo3  2849  ssrab  3018  rexun  3123  elin3  3128  inass  3147  unssdif  3172  indifdir  3193  difin2  3199  inrab2  3210  rabun2  3216  reuun2  3220  undif4  3284  rexsns  3409  rexsnsOLD  3410  rexdifsn  3499  2ralunsn  3569  iuncom4  3664  iunxiun  3736  inuni  3909  unidif0  3920  bnd2  3926  otth2  3978  copsexg  3981  copsex4g  3984  opeqsn  3989  opelopabsbALT  3996  suc11g  4281  rabxp  4380  opeliunxp  4395  xpundir  4397  xpiundi  4398  xpiundir  4399  brinxp2  4407  rexiunxp  4478  brres  4618  brresg  4620  dmres  4632  resiexg  4653  dminss  4738  imainss  4739  ssrnres  4763  elxp4  4808  elxp5  4809  cnvresima  4810  coundi  4822  resco  4825  imaco  4826  coiun  4830  coi1  4836  coass  4839  xpcom  4864  dffun2  4912  fncnv  4965  imadiflem  4978  imadif  4979  imainlem  4980  mptun  5029  fcnvres  5073  dff1o2  5131  dff1o3  5132  ffoss  5158  f11o  5159  brprcneu  5171  fvun2  5240  eqfnfv3  5267  respreima  5295  f1ompt  5320  fsn  5335  abrexco  5398  imaiun  5399  f1mpt  5410  dff1o6  5416  oprabid  5537  dfoprab2  5552  oprab4  5575  mpt2mptx  5595  opabex3d  5748  opabex3  5749  abexssex  5752  dfopab2  5815  dfoprab3s  5816  1stconst  5842  2ndconst  5843  xporderlem  5852  brtpos2  5866  tpostpos  5879  tposmpt2  5896  oviec  6212  domen  6232  xpsnen  6295  xpcomco  6300  xpassen  6304  ltexpi  6435  dfmq0qs  6527  dfplq0qs  6528  enq0enq  6529  enq0ref  6531  enq0tr  6532  nqnq0pi  6536  prnmaxl  6586  prnminu  6587  addsrpr  6830  mulsrpr  6831  addcnsr  6910  mulcnsr  6911  ltresr  6915  addvalex  6920  axprecex  6954  elnnz  8255  fnn0ind  8354  rexuz2  8524  qreccl  8576  rexrp  8605  elixx3g  8770  elfz2  8881  elfzuzb  8884  fznn  8951  elfz2nn0  8973  fznn0  8974  4fvwrd4  8997  elfzo2  9007  fzind2  9095  cvg1nlemres  9584  bdcriota  10003  bj-peano4  10080  alsconv  10119