Theorem anbi1i 446

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anbi2ci  447  anbi12i  448  an12  526  anandi  555  pm5.53  749  pm5.75  904  3ancoma  927  3ioran  935  an6  1253  19.26-3an  1413  19.28h  1495  19.28  1496  eeeanv  1850  sb3an  1874  moanim  2016  nfrexdya  2402  r19.26-3  2488  r19.41  2510  rexcomf  2517  3reeanv  2525  cbvreu  2576  ceqsex3v  2642  rexab  2755  rexrab  2756  rmo4  2786  reuind  2796  sbc3an  2876  rmo3  2906  ssrab  3073  rexun  3153  elin3  3164  inass  3183  unssdif  3206  indifdir  3227  difin2  3233  inrab2  3244  rabun2  3250  reuun2  3254  undif4  3313  rexsns  3440  rexdifsn  3529  2ralunsn  3598  iuncom4  3693  iunxiun  3765  inuni  3938  unidif0  3949  bnd2  3955  otth2  4004  copsexg  4007  copsex4g  4010  opeqsn  4015  opelopabsbALT  4022  suc11g  4308  rabxp  4406  opeliunxp  4421  xpundir  4423  xpiundi  4424  xpiundir  4425  brinxp2  4433  rexiunxp  4506  brres  4646  brresg  4648  dmres  4660  resiexg  4683  dminss  4768  imainss  4769  ssrnres  4793  elxp4  4838  elxp5  4839  cnvresima  4840  coundi  4852  resco  4855  imaco  4856  coiun  4860  coi1  4866  coass  4869  xpcom  4894  dffun2  4942  fncnv  4996  imadiflem  5009  imadif  5010  imainlem  5011  mptun  5060  fcnvres  5104  dff1o2  5162  dff1o3  5163  ffoss  5189  f11o  5190  brprcneu  5202  fvun2  5272  eqfnfv3  5299  respreima  5327  f1ompt  5352  fsn  5367  abrexco  5430  imaiun  5431  f1mpt  5442  dff1o6  5447  oprabid  5568  dfoprab2  5583  oprab4  5606  mpt2mptx  5626  opabex3d  5779  opabex3  5780  abexssex  5783  dfopab2  5846  dfoprab3s  5847  1stconst  5873  2ndconst  5874  xporderlem  5883  spc2ed  5885  f1od2  5887  brtpos2  5900  tpostpos  5913  tposmpt2  5930  oviec  6278  domen  6298  xpsnen  6365  xpcomco  6370  xpassen  6374  ltexpi  6589  dfmq0qs  6681  dfplq0qs  6682  enq0enq  6683  enq0ref  6685  enq0tr  6686  nqnq0pi  6690  prnmaxl  6740  prnminu  6741  addsrpr  6984  mulsrpr  6985  addcnsr  7064  mulcnsr  7065  ltresr  7069  addvalex  7074  axprecex  7108  elnnz  8442  fnn0ind  8544  rexuz2  8750  qreccl  8808  rexrp  8837  elixx3g  9000  elfz2  9112  elfzuzb  9115  fznn  9182  elfz2nn0  9205  fznn0  9206  4fvwrd4  9227  elfzo2  9237  fzind2  9325  cvg1nlemres  10009  divalgb  10469  bezoutlemmain  10531  isprm2  10643  oddpwdc  10696  bdcriota  10832  bj-peano4  10908  alsconv  10949