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  3800  2ralunsn  3877  iuncom4  3972  iunxiun  4047  inuni  4239  unidif0  4251  bnd2  4257  otth2  4327  copsexg  4330  copsex4g  4333  opeqsn  4339  opelopabsbALT  4347  elpwpwel  4566  suc11g  4649  rabxp  4756  opeliunxp  4774  xpundir  4776  xpiundi  4777  xpiundir  4778  brinxp2  4786  rexiunxp  4864  brres  5011  brresg  5013  dmres  5026  resiexg  5050  dminss  5143  imainss  5144  ssrnres  5171  elxp4  5216  elxp5  5217  cnvresima  5218  coundi  5230  resco  5233  imaco  5234  coiun  5238  coi1  5244  coass  5247  xpcom  5275  dffun2  5328  fncnv  5387  imadiflem  5400  imadif  5401  imainlem  5402  mptun  5455  fcnvres  5511  dff1o2  5579  dff1o3  5580  ffoss  5606  f11o  5607  brprcneu  5622  fvun2  5703  eqfnfv3  5736  respreima  5765  f1ompt  5788  fsn  5809  abrexco  5889  imaiun  5890  f1mpt  5901  dff1o6  5906  oprabid  6039  dfoprab2  6057  oprab4  6081  mpomptx  6101  opabex3d  6272  opabex3  6273  abexssex  6276  dfopab2  6341  dfoprab3s  6342  1stconst  6373  2ndconst  6374  xporderlem  6383  spc2ed  6385  f1od2  6387  brtpos2  6403  tpostpos  6416  tposmpo  6433  oviec  6796  mapsncnv  6850  dfixp  6855  domen  6908  mapsnen  6972  xpsnen  6988  xpcomco  6993  xpassen  6997  ltexpi  7535  dfmq0qs  7627  dfplq0qs  7628  enq0enq  7629  enq0ref  7631  enq0tr  7632  nqnq0pi  7636  prnmaxl  7686  prnminu  7687  suplocexprlemloc  7919  addsrpr  7943  mulsrpr  7944  suplocsrlemb  8004  addcnsr  8032  mulcnsr  8033  ltresr  8037  addvalex  8042  axprecex  8078  elnnz  9467  fnn0ind  9574  rexuz2  9788  qreccl  9849  rexrp  9884  elixx3g  10109  elfz2  10223  elfzuzb  10227  fznn  10297  elfz2nn0  10320  fznn0  10321  4fvwrd4  10348  elfzo2  10358  fzind2  10457  cvg1nlemres  11511  fsum2dlemstep  11960  modfsummod  11984  fprodseq  12109  divalgb  12451  bezoutlemmain  12534  isprm2  12654  oddpwdc  12711  prdsex  13317  prdsval  13321  prdsbaslemss  13322  xpscf  13395  issubg3  13744  releqgg  13772  eqgex  13773  imasabl  13888  dfrhm2  14133  ntreq0  14821  cnnei  14921  txlm  14968  blres  15123  isms2  15143  dedekindicclemicc  15321  limcrcl  15347  lgsquadlem1  15771  lgsquadlem2  15772  bdcriota  16301  bj-peano4  16373  alsconv  16508