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	⊢ (𝜑 ↔ 𝜓)

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 455	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))

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  592  pm5.53  807  pm5.75  968  3ancoma  1009  3ioran  1017  an6  1355  19.26-3an  1529  19.28h  1608  19.28  1609  eeeanv  1984  sb3an  2009  moanim  2152  nfrexdya  2566  r19.26-3  2661  r19.41  2686  rexcomf  2693  3reeanv  2702  cbvreu  2763  ceqsex3v  2843  rexab  2965  rexrab  2966  rmo4  2996  rmo3f  3000  reuind  3008  sbc3an  3090  rmo3  3121  ssrab  3302  rexun  3384  elin3  3395  inass  3414  unssdif  3439  indifdir  3460  difin2  3466  inrab2  3477  rabun2  3483  reuun2  3487  undif4  3554  rexdifpr  3694  rexsns  3705  rexdifsn  3799  2ralunsn  3876  iuncom4  3971  iunxiun  4046  inuni  4238  unidif0  4250  bnd2  4256  otth2  4326  copsexg  4329  copsex4g  4332  opeqsn  4338  opelopabsbALT  4346  elpwpwel  4565  suc11g  4648  rabxp  4755  opeliunxp  4773  xpundir  4775  xpiundi  4776  xpiundir  4777  brinxp2  4785  rexiunxp  4863  brres  5010  brresg  5012  dmres  5025  resiexg  5049  dminss  5142  imainss  5143  ssrnres  5170  elxp4  5215  elxp5  5216  cnvresima  5217  coundi  5229  resco  5232  imaco  5233  coiun  5237  coi1  5243  coass  5246  xpcom  5274  dffun2  5327  fncnv  5386  imadiflem  5399  imadif  5400  imainlem  5401  mptun  5454  fcnvres  5508  dff1o2  5576  dff1o3  5577  ffoss  5603  f11o  5604  brprcneu  5619  fvun2  5700  eqfnfv3  5733  respreima  5762  f1ompt  5785  fsn  5806  abrexco  5882  imaiun  5883  f1mpt  5894  dff1o6  5899  oprabid  6032  dfoprab2  6050  oprab4  6074  mpomptx  6094  opabex3d  6264  opabex3  6265  abexssex  6268  dfopab2  6333  dfoprab3s  6334  1stconst  6365  2ndconst  6366  xporderlem  6375  spc2ed  6377  f1od2  6379  brtpos2  6395  tpostpos  6408  tposmpo  6425  oviec  6786  mapsncnv  6840  dfixp  6845  domen  6898  mapsnen  6962  xpsnen  6976  xpcomco  6981  xpassen  6985  ltexpi  7520  dfmq0qs  7612  dfplq0qs  7613  enq0enq  7614  enq0ref  7616  enq0tr  7617  nqnq0pi  7621  prnmaxl  7671  prnminu  7672  suplocexprlemloc  7904  addsrpr  7928  mulsrpr  7929  suplocsrlemb  7989  addcnsr  8017  mulcnsr  8018  ltresr  8022  addvalex  8027  axprecex  8063  elnnz  9452  fnn0ind  9559  rexuz2  9772  qreccl  9833  rexrp  9868  elixx3g  10093  elfz2  10207  elfzuzb  10211  fznn  10281  elfz2nn0  10304  fznn0  10305  4fvwrd4  10332  elfzo2  10342  fzind2  10440  cvg1nlemres  11491  fsum2dlemstep  11940  modfsummod  11964  fprodseq  12089  divalgb  12431  bezoutlemmain  12514  isprm2  12634  oddpwdc  12691  prdsex  13297  prdsval  13301  prdsbaslemss  13302  xpscf  13375  issubg3  13724  releqgg  13752  eqgex  13753  imasabl  13868  dfrhm2  14112  ntreq0  14800  cnnei  14900  txlm  14947  blres  15102  isms2  15122  dedekindicclemicc  15300  limcrcl  15326  lgsquadlem1  15750  lgsquadlem2  15751  bdcriota  16204  bj-peano4  16276  alsconv  16407