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  563  anandi  594  pm5.53  810  pm5.75  971  3ancoma  1012  3ioran  1020  an6  1358  19.26-3an  1532  19.28h  1611  19.28  1612  eeeanv  1986  sb3an  2011  moanim  2154  nfrexdya  2569  r19.26-3  2664  r19.41  2689  rexcomf  2696  3reeanv  2705  cbvreu  2766  ceqsex3v  2847  rexab  2969  rexrab  2970  rmo4  3000  rmo3f  3004  reuind  3012  sbc3an  3094  rmo3  3125  ssrab  3306  rexun  3389  elin3  3400  inass  3419  unssdif  3444  indifdir  3465  difin2  3471  inrab2  3482  rabun2  3488  reuun2  3492  undif4  3559  rexdifpr  3701  rexsns  3712  rexdifsn  3809  2ralunsn  3887  iuncom4  3982  iunxiun  4057  inuni  4250  unidif0  4263  bnd2  4269  otth2  4339  copsexg  4342  copsex4g  4345  opeqsn  4351  opelopabsbALT  4359  elpwpwel  4578  suc11g  4661  rabxp  4769  opeliunxp  4787  xpundir  4789  xpiundi  4790  xpiundir  4791  brinxp2  4799  rexiunxp  4878  brres  5025  brresg  5027  dmres  5040  resiexg  5064  dminss  5158  imainss  5159  ssrnres  5186  elxp4  5231  elxp5  5232  cnvresima  5233  coundi  5245  resco  5248  imaco  5249  coiun  5253  coi1  5259  coass  5262  xpcom  5290  dffun2  5343  fncnv  5403  imadiflem  5416  imadif  5417  imainlem  5418  mptun  5471  fcnvres  5528  dff1o2  5597  dff1o3  5598  ffoss  5625  f11o  5626  brprcneu  5641  fvun2  5722  eqfnfv3  5755  respreima  5783  f1ompt  5806  fsn  5827  abrexco  5910  imaiun  5911  f1mpt  5922  dff1o6  5927  oprabid  6060  dfoprab2  6078  oprab4  6102  mpomptx  6122  opabex3d  6292  opabex3  6293  abexssex  6296  dfopab2  6361  dfoprab3s  6362  1stconst  6395  2ndconst  6396  xporderlem  6405  spc2ed  6407  f1od2  6409  brtpos2  6460  tpostpos  6473  tposmpo  6490  oviec  6853  mapsncnv  6907  dfixp  6912  domen  6965  mapsnen  7029  xpsnen  7048  xpcomco  7053  xpassen  7057  sspw1or2  7446  ltexpi  7600  dfmq0qs  7692  dfplq0qs  7693  enq0enq  7694  enq0ref  7696  enq0tr  7697  nqnq0pi  7701  prnmaxl  7751  prnminu  7752  suplocexprlemloc  7984  addsrpr  8008  mulsrpr  8009  suplocsrlemb  8069  addcnsr  8097  mulcnsr  8098  ltresr  8102  addvalex  8107  axprecex  8143  elnnz  9533  fnn0ind  9640  rexuz2  9859  qreccl  9920  rexrp  9955  elixx3g  10180  elfz2  10295  elfzuzb  10299  fznn  10369  elfz2nn0  10392  fznn0  10393  4fvwrd4  10420  elfzo2  10430  fzind2  10531  cvg1nlemres  11608  fsum2dlemstep  12058  modfsummod  12082  fprodseq  12207  divalgb  12549  bezoutlemmain  12632  isprm2  12752  oddpwdc  12809  prdsex  13415  prdsval  13419  prdsbaslemss  13420  xpscf  13493  issubg3  13842  releqgg  13870  eqgex  13871  imasabl  13986  dfrhm2  14232  ntreq0  14926  cnnei  15026  txlm  15073  blres  15228  isms2  15248  dedekindicclemicc  15426  limcrcl  15452  lgsquadlem1  15879  lgsquadlem2  15880  isclwwlknx  16340  clwwlknonel  16356  clwwlknon2x  16359  iseupthf1o  16372  bdcriota  16582  bj-peano4  16654  alsconv  16806