Theorem anbi1i 462

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 9	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.32ri 459	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi2ci  463  anbi12i  464  bianassc  474  an12  567  anandi  598  pm5.53  814  pm5.75  975  3ancoma  1016  3ioran  1024  an6  1362  19.26-3an  1536  19.28h  1615  19.28  1616  eeeanv  1993  sb3an  2018  moanim  2161  nfrexdya  2586  r19.26-3  2681  r19.41  2706  rexcomf  2713  3reeanv  2722  cbvreu  2784  ceqsex3v  2865  rexab  2988  rexrab  2989  rmo4  3019  rmo3f  3023  reuind  3031  sbc3an  3113  rmo3  3144  ssrab  3326  rexun  3409  elin3  3420  inass  3441  unssdif  3466  indifdir  3487  difin2  3493  inrab2  3506  rabun2  3512  reuun2  3516  undif4  3587  rexdifpr  3737  rexsns  3748  rexdifsn  3846  2ralunsn  3924  iuncom4  4019  iunxiun  4094  inuni  4293  unidif0  4306  bnd2  4312  otth2  4383  copsexg  4386  copsex4g  4389  opeqsn  4395  opelopabsbALT  4403  elpwpwel  4623  suc11g  4706  rabxp  4814  opeliunxp  4832  xpundir  4834  xpiundi  4835  xpiundir  4836  brinxp2  4844  rexiunxp  4924  brres  5071  brresg  5073  dmres  5086  resiexg  5111  dminss  5205  imainss  5206  ssrnres  5233  elxp4  5278  elxp5  5279  cnvresima  5280  coundi  5292  resco  5295  imaco  5296  coiun  5300  coi1  5306  coass  5309  xpcom  5337  dffun2  5390  fncnv  5450  imadiflem  5463  imadif  5464  imainlem  5465  mptun  5518  fcnvres  5578  dff1o2  5647  dff1o3  5648  ffoss  5675  f11o  5676  brprcneu  5691  fvun2  5773  eqfnfv3  5811  respreima  5839  f1ompt  5862  fsn  5883  abrexco  5968  imaiun  5969  f1mpt  5980  dff1o6  5985  oprabid  6120  dfoprab2  6138  oprab4  6162  mpomptx  6182  opabex3d  6354  opabex3  6355  abexssex  6358  dfopab2  6427  dfoprab3s  6428  1stconst  6461  2ndconst  6462  xporderlem  6471  spc2ed  6473  f1od2  6475  brtpos2  6527  tpostpos  6540  tposmpo  6557  oviec  6920  mapsncnv  6983  dfixp  6988  domen  7041  mapsnen  7106  xpsnen  7125  xpcomco  7130  xpassen  7134  sspw1or2  7550  ltexpi  7710  dfmq0qs  7802  dfplq0qs  7803  enq0enq  7804  enq0ref  7806  enq0tr  7807  nqnq0pi  7811  prnmaxl  7861  prnminu  7862  suplocexprlemloc  8094  addsrpr  8118  mulsrpr  8119  suplocsrlemb  8179  addcnsr  8207  mulcnsr  8208  ltresr  8212  addvalex  8217  axprecex  8253  elnnz  9663  fnn0ind  9772  rexuz2  9996  qreccl  10057  rexrp  10093  elixx3g  10319  elfz2  10434  elfzuzb  10438  fznn  10512  elfz2nn0  10535  fznn0  10536  4fvwrd4  10563  elfzo2  10573  fzind2  10674  sseqn  11300  hashf1lem1  11306  hashf1lem2  11307  cvg1nlemres  11772  fsum2dlemstep  12225  modfsummod  12249  fprodseq  12374  divalgb  12716  bezoutlemmain  12799  isprm2  12919  nnmaxpw  12977  ballotfilemelo  13279  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  xpscf  13726  issubg3  14053  releqgg  14081  eqgex  14082  imasabl  14229  prdsex  14278  prdsval  14279  prdsbaslemss  14280  dfrhm2  14569  drngprop  14725  isassa  15110  ntreq0  15375  cnnei  15475  txlm  15522  blres  15677  isms2  15697  dedekindicclemicc  15875  limcrcl  15901  lgsquadlem1  16418  lgsquadlem2  16419  isclwwlknx  16879  clwwlknonel  16895  clwwlknon2x  16898  iseupthf1o  16911  bdcriota  17131  bj-peano4  17203  alsanmo  17375  ralsanmo  17376  alsralrex  17377  alsraln0m  17378