Theorem anbi1i 676

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	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
anbi1i	⊢ ((φ ∧ χ) ↔ (ψ ∧ χ))

Proof of Theorem anbi1i

Step	Hyp	Ref	Expression
1		bi.aa	. . 3 ⊢ (φ ↔ ψ)
2	1	a1i 10	. 2 ⊢ (χ → (φ ↔ ψ))
3	2	pm5.32ri 619	1 ⊢ ((φ ∧ χ) ↔ (ψ ∧ χ))

Syntax hints:   ↔ wb 176   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  anbi2ci  677  anbi12i  678  pm5.53  771  an12  772  anandi  801  pm5.75  903  3ancoma  941  3ioran  950  an6  1261  19.26-3an  1595  19.28  1870  eeeanv  1914  sb3an  2070  pm11.07  2115  2eu6  2289  r19.26-3  2749  r19.41  2764  rexcomf  2771  3reeanv  2780  cbvreu  2834  ceqsex3v  2898  rexab  3000  rexrab  3001  rmo4  3030  reuind  3040  rmo3  3134  ssrab  3345  rexun  3444  elin3  3448  inass  3466  dfun2  3491  indifdir  3512  difin2  3517  inrab2  3529  rabun2  3535  reuun2  3539  undif4  3608  difin0ss  3617  rexsns  3765  rexdifsn  3844  2ralunsn  3881  iuncom4  3977  iunxiun  4049  axxpprim  4091  axcnvprim  4092  axssetprim  4093  axsiprim  4094  axtyplowerprim  4095  axins2prim  4096  axins3prim  4097  elpw12  4146  elpw11c  4148  elpw121c  4149  elpw131c  4150  elpw141c  4151  elpw151c  4152  elpw161c  4153  elpw171c  4154  elpw181c  4155  elpw191c  4156  elpw1101c  4157  elpw1111c  4158  pw1in  4165  eluni1g  4173  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  opkelimagekg  4272  imacok  4283  dfimak2  4299  insklem  4305  ndisjrelk  4324  unipw1  4326  dfpw2  4328  dfaddc2  4382  dfnnc2  4396  elsuc  4414  addcass  4416  nnsucelrlem1  4425  ltfinex  4465  ssfin  4471  eqpwrelk  4479  eqpw1relk  4480  ncfinraiselem2  4481  ncfinlowerlem1  4483  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  spfinex  4538  vfinspsslem1  4551  vfinspss  4552  vfinspclt  4553  vfinncsp  4555  dfop2lem1  4574  copsexg  4608  copsex4g  4611  br1stg  4731  setconslem1  4732  setconslem2  4733  setconslem3  4734  setconslem4  4735  setconslem6  4737  setconslem7  4738  df1st2  4739  dfswap2  4742  dfid3  4769  opelxp  4812  rabxp  4815  xpiundi  4818  xpiundir  4819  opeliunxp  4821  eliunxp  4822  xpundir  4834  brinxp2  4836  brswap2  4861  dmuni  4915  elimapw1  4945  elimapw12  4946  elimapw13  4947  elimapw11c  4949  opelres  4951  dmres  4987  iss  5001  rnuni  5039  dminss  5042  imainss  5043  ssrnres  5060  cnvresima  5078  coundi  5083  resco  5086  imaco  5087  coiun  5091  coi1  5095  coass  5098  dfcnv2  5101  elxp4  5109  df2nd2  5112  dffun2  5120  fncnv  5159  imadif  5172  fcnvres  5244  dff1o2  5292  dff1o3  5293  f1ores  5301  ffoss  5315  f11o  5316  fvun2  5381  eqfnfv3  5395  respreima  5411  fopabfv  5431  fsn  5433  abrexco  5464  imaiun  5465  dff1o6  5476  isoini  5498  oprabid  5551  oprab4  5567  eloprabga  5579  fnov  5592  fov  5593  mpt2mptx  5709  brsnsi2  5777  brco1st  5778  brco2nd  5779  trtxp  5782  restxp  5787  elfix  5788  brimage  5794  oqelins4  5795  txpcofun  5804  otsnelsi3  5806  addcfnex  5825  qrpprod  5837  brpprod  5840  dmpprod  5841  pw1fnf1o  5856  clos1ex  5877  clos1induct  5881  clos1is  5882  porta  5934  mapexi  6004  map0e  6024  fundmen  6044  unen  6049  xpassenlem  6057  xpassen  6058  enpw1lem1  6062  enmap2lem1  6064  enmap1lem1  6070  enpw1pw  6076  lecex  6116  ceexlem1  6174  el2c  6192  sbthlem1  6204  sbthlem3  6206  taddc  6230  tcfnex  6245  csucex  6260  addccan2nclem1  6264  nmembers1lem1  6269  nncdiv3lem1  6276  nnc3n3p1  6279  spacvallem1  6282  nchoicelem11  6300  nchoicelem16  6305  fnfreclem2  6319  fnfreclem3  6320