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	|- (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 10	. 2 |- (ch -> (ph <-> ps))
3	2	pm5.32ri 619	1 |- ((ph /\ ch) <-> (ps /\ ch))

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  2748  r19.41  2763  rexcomf  2770  3reeanv  2779  cbvreu  2833  ceqsex3v  2897  rexab  2999  rexrab  3000  rmo4  3029  reuind  3039  rmo3  3133  ssrab  3344  rexun  3443  elin3  3447  inass  3465  dfun2  3490  indifdir  3511  difin2  3516  inrab2  3528  rabun2  3534  reuun2  3538  undif4  3607  difin0ss  3616  rexsns  3764  rexdifsn  3843  2ralunsn  3880  iuncom4  3976  iunxiun  4048  axxpprim  4090  axcnvprim  4091  axssetprim  4092  axsiprim  4093  axtyplowerprim  4094  axins2prim  4095  axins3prim  4096  elpw12  4145  elpw11c  4147  elpw121c  4148  elpw131c  4149  elpw141c  4150  elpw151c  4151  elpw161c  4152  elpw171c  4153  elpw181c  4154  elpw191c  4155  elpw1101c  4156  elpw1111c  4157  pw1in  4164  eluni1g  4172  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  opkelimagekg  4271  imacok  4282  dfimak2  4298  insklem  4304  ndisjrelk  4323  unipw1  4325  dfpw2  4327  dfaddc2  4381  dfnnc2  4395  elsuc  4413  addcass  4415  nnsucelrlem1  4424  ltfinex  4464  ssfin  4470  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinlowerlem1  4482  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  nnpweqlem1  4522  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  spfinex  4537  vfinspsslem1  4550  vfinspss  4551  vfinspclt  4552  vfinncsp  4554  dfop2lem1  4573  copsexg  4607  copsex4g  4610  br1stg  4730  setconslem1  4731  setconslem2  4732  setconslem3  4733  setconslem4  4734  setconslem6  4736  setconslem7  4737  df1st2  4738  dfswap2  4741  dfid3  4768  opelxp  4811  rabxp  4814  xpiundi  4817  xpiundir  4818  opeliunxp  4820  eliunxp  4821  xpundir  4833  brinxp2  4835  brswap2  4860  dmuni  4914  elimapw1  4944  elimapw12  4945  elimapw13  4946  elimapw11c  4948  opelres  4950  dmres  4986  iss  5000  rnuni  5038  dminss  5041  imainss  5042  ssrnres  5059  cnvresima  5077  coundi  5082  resco  5085  imaco  5086  coiun  5090  coi1  5094  coass  5097  dfcnv2  5100  elxp4  5108  df2nd2  5111  dffun2  5119  fncnv  5158  imadif  5171  fcnvres  5243  dff1o2  5291  dff1o3  5292  f1ores  5300  ffoss  5314  f11o  5315  fvun2  5380  eqfnfv3  5394  respreima  5410  fopabfv  5430  fsn  5432  abrexco  5463  imaiun  5464  dff1o6  5475  isoini  5497  oprabid  5550  oprab4  5566  eloprabga  5578  fnov  5591  fov  5592  mpt2mptx  5708  brsnsi2  5776  brco1st  5777  brco2nd  5778  trtxp  5781  restxp  5786  elfix  5787  brimage  5793  oqelins4  5794  txpcofun  5803  otsnelsi3  5805  addcfnex  5824  qrpprod  5836  brpprod  5839  dmpprod  5840  pw1fnf1o  5855  clos1ex  5876  clos1induct  5880  clos1is  5881  porta  5933  mapexi  6003  map0e  6023  fundmen  6043  unen  6048  xpassenlem  6056  xpassen  6057  enpw1lem1  6061  enmap2lem1  6063  enmap1lem1  6069  enpw1pw  6075  lecex  6115  ceexlem1  6173  el2c  6191  sbthlem1  6203  sbthlem3  6205  taddc  6229  tcfnex  6244  csucex  6259  addccan2nclem1  6263  nmembers1lem1  6268  nncdiv3lem1  6275  nnc3n3p1  6278  spacvallem1  6281  nchoicelem11  6299  nchoicelem16  6304  fnfreclem2  6318  fnfreclem3  6319