Theorem anbi1i 451

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

Syntax hints:   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi2ci  452  anbi12i  453  an12  533  anandi  562  pm5.53  774  pm5.75  927  3ancoma  950  3ioran  958  an6  1280  19.26-3an  1440  19.28h  1522  19.28  1523  eeeanv  1881  sb3an  1905  moanim  2047  nfrexdya  2442  r19.26-3  2534  r19.41  2558  rexcomf  2565  3reeanv  2573  cbvreu  2624  ceqsex3v  2697  rexab  2813  rexrab  2814  rmo4  2844  rmo3f  2848  reuind  2856  sbc3an  2936  rmo3  2966  ssrab  3139  rexun  3220  elin3  3231  inass  3250  unssdif  3275  indifdir  3296  difin2  3302  inrab2  3313  rabun2  3319  reuun2  3323  undif4  3389  rexsns  3527  rexdifsn  3619  2ralunsn  3689  iuncom4  3784  iunxiun  3858  inuni  4038  unidif0  4049  bnd2  4055  otth2  4121  copsexg  4124  copsex4g  4127  opeqsn  4132  opelopabsbALT  4139  elpwpwel  4354  suc11g  4430  rabxp  4534  opeliunxp  4552  xpundir  4554  xpiundi  4555  xpiundir  4556  brinxp2  4564  rexiunxp  4639  brres  4781  brresg  4783  dmres  4796  resiexg  4820  dminss  4909  imainss  4910  ssrnres  4937  elxp4  4982  elxp5  4983  cnvresima  4984  coundi  4996  resco  4999  imaco  5000  coiun  5004  coi1  5010  coass  5013  xpcom  5041  dffun2  5089  fncnv  5145  imadiflem  5158  imadif  5159  imainlem  5160  mptun  5210  fcnvres  5262  dff1o2  5326  dff1o3  5327  ffoss  5353  f11o  5354  brprcneu  5366  fvun2  5440  eqfnfv3  5472  respreima  5500  f1ompt  5523  fsn  5544  abrexco  5612  imaiun  5613  f1mpt  5624  dff1o6  5629  oprabid  5755  dfoprab2  5770  oprab4  5794  mpomptx  5814  opabex3d  5970  opabex3  5971  abexssex  5974  dfopab2  6038  dfoprab3s  6039  1stconst  6069  2ndconst  6070  xporderlem  6079  spc2ed  6081  f1od2  6083  brtpos2  6099  tpostpos  6112  tposmpo  6129  oviec  6486  mapsncnv  6540  dfixp  6545  domen  6596  mapsnen  6656  xpsnen  6665  xpcomco  6670  xpassen  6674  ltexpi  7086  dfmq0qs  7178  dfplq0qs  7179  enq0enq  7180  enq0ref  7182  enq0tr  7183  nqnq0pi  7187  prnmaxl  7237  prnminu  7238  addsrpr  7481  mulsrpr  7482  addcnsr  7562  mulcnsr  7563  ltresr  7567  addvalex  7572  axprecex  7608  elnnz  8961  fnn0ind  9064  rexuz2  9271  qreccl  9329  rexrp  9358  elixx3g  9570  elfz2  9683  elfzuzb  9686  fznn  9755  elfz2nn0  9778  fznn0  9779  4fvwrd4  9803  elfzo2  9813  fzind2  9902  cvg1nlemres  10642  fsum2dlemstep  11088  modfsummod  11112  divalgb  11463  bezoutlemmain  11525  isprm2  11637  oddpwdc  11690  ntreq0  12137  cnnei  12236  txlm  12283  blres  12416  isms2  12436  limcrcl  12576  bdcriota  12760  bj-peano4  12832  alsconv  12922