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  2844  rexab  2966  rexrab  2967  rmo4  2997  rmo3f  3001  reuind  3009  sbc3an  3091  rmo3  3122  ssrab  3303  rexun  3385  elin3  3396  inass  3415  unssdif  3440  indifdir  3461  difin2  3467  inrab2  3478  rabun2  3484  reuun2  3488  undif4  3555  rexdifpr  3695  rexsns  3706  rexdifsn  3803  2ralunsn  3880  iuncom4  3975  iunxiun  4050  inuni  4243  unidif0  4255  bnd2  4261  otth2  4331  copsexg  4334  copsex4g  4337  opeqsn  4343  opelopabsbALT  4351  elpwpwel  4570  suc11g  4653  rabxp  4761  opeliunxp  4779  xpundir  4781  xpiundi  4782  xpiundir  4783  brinxp2  4791  rexiunxp  4870  brres  5017  brresg  5019  dmres  5032  resiexg  5056  dminss  5149  imainss  5150  ssrnres  5177  elxp4  5222  elxp5  5223  cnvresima  5224  coundi  5236  resco  5239  imaco  5240  coiun  5244  coi1  5250  coass  5253  xpcom  5281  dffun2  5334  fncnv  5393  imadiflem  5406  imadif  5407  imainlem  5408  mptun  5461  fcnvres  5517  dff1o2  5585  dff1o3  5586  ffoss  5612  f11o  5613  brprcneu  5628  fvun2  5709  eqfnfv3  5742  respreima  5771  f1ompt  5794  fsn  5815  abrexco  5895  imaiun  5896  f1mpt  5907  dff1o6  5912  oprabid  6045  dfoprab2  6063  oprab4  6087  mpomptx  6107  opabex3d  6278  opabex3  6279  abexssex  6282  dfopab2  6347  dfoprab3s  6348  1stconst  6381  2ndconst  6382  xporderlem  6391  spc2ed  6393  f1od2  6395  brtpos2  6412  tpostpos  6425  tposmpo  6442  oviec  6805  mapsncnv  6859  dfixp  6864  domen  6917  mapsnen  6981  xpsnen  7000  xpcomco  7005  xpassen  7009  ltexpi  7547  dfmq0qs  7639  dfplq0qs  7640  enq0enq  7641  enq0ref  7643  enq0tr  7644  nqnq0pi  7648  prnmaxl  7698  prnminu  7699  suplocexprlemloc  7931  addsrpr  7955  mulsrpr  7956  suplocsrlemb  8016  addcnsr  8044  mulcnsr  8045  ltresr  8049  addvalex  8054  axprecex  8090  elnnz  9479  fnn0ind  9586  rexuz2  9805  qreccl  9866  rexrp  9901  elixx3g  10126  elfz2  10240  elfzuzb  10244  fznn  10314  elfz2nn0  10337  fznn0  10338  4fvwrd4  10365  elfzo2  10375  fzind2  10475  cvg1nlemres  11536  fsum2dlemstep  11985  modfsummod  12009  fprodseq  12134  divalgb  12476  bezoutlemmain  12559  isprm2  12679  oddpwdc  12736  prdsex  13342  prdsval  13346  prdsbaslemss  13347  xpscf  13420  issubg3  13769  releqgg  13797  eqgex  13798  imasabl  13913  dfrhm2  14158  ntreq0  14846  cnnei  14946  txlm  14993  blres  15148  isms2  15168  dedekindicclemicc  15346  limcrcl  15372  lgsquadlem1  15796  lgsquadlem2  15797  isclwwlknx  16211  clwwlknonel  16227  clwwlknon2x  16230  iseupthf1o  16243  bdcriota  16414  bj-peano4  16486  alsconv  16620