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  803  pm5.75  964  3ancoma  987  3ioran  995  an6  1332  19.26-3an  1494  19.28h  1573  19.28  1574  eeeanv  1945  sb3an  1970  moanim  2112  nfrexdya  2526  r19.26-3  2620  r19.41  2645  rexcomf  2652  3reeanv  2661  cbvreu  2716  ceqsex3v  2794  rexab  2914  rexrab  2915  rmo4  2945  rmo3f  2949  reuind  2957  sbc3an  3039  rmo3  3069  ssrab  3248  rexun  3330  elin3  3341  inass  3360  unssdif  3385  indifdir  3406  difin2  3412  inrab2  3423  rabun2  3429  reuun2  3433  undif4  3500  rexdifpr  3635  rexsns  3646  rexdifsn  3739  2ralunsn  3813  iuncom4  3908  iunxiun  3983  inuni  4170  unidif0  4182  bnd2  4188  otth2  4256  copsexg  4259  copsex4g  4262  opeqsn  4267  opelopabsbALT  4274  elpwpwel  4490  suc11g  4571  rabxp  4678  opeliunxp  4696  xpundir  4698  xpiundi  4699  xpiundir  4700  brinxp2  4708  rexiunxp  4784  brres  4928  brresg  4930  dmres  4943  resiexg  4967  dminss  5058  imainss  5059  ssrnres  5086  elxp4  5131  elxp5  5132  cnvresima  5133  coundi  5145  resco  5148  imaco  5149  coiun  5153  coi1  5159  coass  5162  xpcom  5190  dffun2  5241  fncnv  5297  imadiflem  5310  imadif  5311  imainlem  5312  mptun  5362  fcnvres  5414  dff1o2  5481  dff1o3  5482  ffoss  5508  f11o  5509  brprcneu  5523  fvun2  5599  eqfnfv3  5631  respreima  5660  f1ompt  5683  fsn  5704  abrexco  5776  imaiun  5777  f1mpt  5788  dff1o6  5793  oprabid  5923  dfoprab2  5938  oprab4  5962  mpomptx  5982  opabex3d  6140  opabex3  6141  abexssex  6144  dfopab2  6208  dfoprab3s  6209  1stconst  6240  2ndconst  6241  xporderlem  6250  spc2ed  6252  f1od2  6254  brtpos2  6270  tpostpos  6283  tposmpo  6300  oviec  6659  mapsncnv  6713  dfixp  6718  domen  6769  mapsnen  6829  xpsnen  6839  xpcomco  6844  xpassen  6848  ltexpi  7354  dfmq0qs  7446  dfplq0qs  7447  enq0enq  7448  enq0ref  7450  enq0tr  7451  nqnq0pi  7455  prnmaxl  7505  prnminu  7506  suplocexprlemloc  7738  addsrpr  7762  mulsrpr  7763  suplocsrlemb  7823  addcnsr  7851  mulcnsr  7852  ltresr  7856  addvalex  7861  axprecex  7897  elnnz  9281  fnn0ind  9387  rexuz2  9599  qreccl  9660  rexrp  9694  elixx3g  9919  elfz2  10033  elfzuzb  10037  fznn  10107  elfz2nn0  10130  fznn0  10131  4fvwrd4  10158  elfzo2  10168  fzind2  10257  cvg1nlemres  11012  fsum2dlemstep  11460  modfsummod  11484  fprodseq  11609  divalgb  11948  bezoutlemmain  12017  isprm2  12135  oddpwdc  12192  prdsex  12740  xpscf  12789  issubg3  13097  releqgg  13125  eqgex  13126  imasabl  13234  dfrhm2  13465  ntreq0  14016  cnnei  14116  txlm  14163  blres  14318  isms2  14338  dedekindicclemicc  14494  limcrcl  14511  bdcriota  15019  bj-peano4  15091  alsconv  15213