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  563  anandi  594  pm5.53  810  pm5.75  971  3ancoma  1012  3ioran  1020  an6  1358  19.26-3an  1532  19.28h  1611  19.28  1612  eeeanv  1987  sb3an  2012  moanim  2155  nfrexdya  2578  r19.26-3  2673  r19.41  2698  rexcomf  2705  3reeanv  2714  cbvreu  2776  ceqsex3v  2857  rexab  2979  rexrab  2980  rmo4  3010  rmo3f  3014  reuind  3022  sbc3an  3104  rmo3  3135  ssrab  3316  rexun  3399  elin3  3410  inass  3431  unssdif  3456  indifdir  3477  difin2  3483  inrab2  3494  rabun2  3500  reuun2  3504  undif4  3571  rexdifpr  3717  rexsns  3728  rexdifsn  3825  2ralunsn  3903  iuncom4  3998  iunxiun  4073  inuni  4267  unidif0  4280  bnd2  4286  otth2  4357  copsexg  4360  copsex4g  4363  opeqsn  4369  opelopabsbALT  4377  elpwpwel  4596  suc11g  4679  rabxp  4787  opeliunxp  4805  xpundir  4807  xpiundi  4808  xpiundir  4809  brinxp2  4817  rexiunxp  4897  brres  5044  brresg  5046  dmres  5059  resiexg  5083  dminss  5177  imainss  5178  ssrnres  5205  elxp4  5250  elxp5  5251  cnvresima  5252  coundi  5264  resco  5267  imaco  5268  coiun  5272  coi1  5278  coass  5281  xpcom  5309  dffun2  5362  fncnv  5422  imadiflem  5435  imadif  5436  imainlem  5437  mptun  5490  fcnvres  5550  dff1o2  5619  dff1o3  5620  ffoss  5647  f11o  5648  brprcneu  5663  fvun2  5744  eqfnfv3  5777  respreima  5805  f1ompt  5828  fsn  5849  abrexco  5932  imaiun  5933  f1mpt  5944  dff1o6  5949  oprabid  6082  dfoprab2  6100  oprab4  6124  mpomptx  6144  opabex3d  6314  opabex3  6315  abexssex  6318  dfopab2  6383  dfoprab3s  6384  1stconst  6417  2ndconst  6418  xporderlem  6427  spc2ed  6429  f1od2  6431  brtpos2  6482  tpostpos  6495  tposmpo  6512  oviec  6875  mapsncnv  6930  dfixp  6935  domen  6988  mapsnen  7053  xpsnen  7072  xpcomco  7077  xpassen  7081  sspw1or2  7495  ltexpi  7652  dfmq0qs  7744  dfplq0qs  7745  enq0enq  7746  enq0ref  7748  enq0tr  7749  nqnq0pi  7753  prnmaxl  7803  prnminu  7804  suplocexprlemloc  8036  addsrpr  8060  mulsrpr  8061  suplocsrlemb  8121  addcnsr  8149  mulcnsr  8150  ltresr  8154  addvalex  8159  axprecex  8195  elnnz  9587  fnn0ind  9694  rexuz2  9913  qreccl  9974  rexrp  10009  elixx3g  10234  elfz2  10349  elfzuzb  10353  fznn  10423  elfz2nn0  10446  fznn0  10447  4fvwrd4  10474  elfzo2  10484  fzind2  10585  sseqn  11203  cvg1nlemres  11670  fsum2dlemstep  12120  modfsummod  12144  fprodseq  12269  divalgb  12611  bezoutlemmain  12694  isprm2  12814  oddpwdc  12871  ballotfilemelo  13141  ballotfilem2  13142  prdsex  13482  prdsval  13486  prdsbaslemss  13487  xpscf  13560  issubg3  13909  releqgg  13937  eqgex  13938  imasabl  14053  dfrhm2  14299  ntreq0  14997  cnnei  15097  txlm  15144  blres  15299  isms2  15319  dedekindicclemicc  15497  limcrcl  15523  lgsquadlem1  15950  lgsquadlem2  15951  isclwwlknx  16411  clwwlknonel  16427  clwwlknon2x  16430  iseupthf1o  16443  bdcriota  16653  bj-peano4  16725  alsconv  16877