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  1989  sb3an  2014  moanim  2157  nfrexdya  2580  r19.26-3  2675  r19.41  2700  rexcomf  2707  3reeanv  2716  cbvreu  2778  ceqsex3v  2859  rexab  2982  rexrab  2983  rmo4  3013  rmo3f  3017  reuind  3025  sbc3an  3107  rmo3  3138  ssrab  3320  rexun  3403  elin3  3414  inass  3435  unssdif  3460  indifdir  3481  difin2  3487  inrab2  3498  rabun2  3504  reuun2  3508  undif4  3575  rexdifpr  3722  rexsns  3733  rexdifsn  3830  2ralunsn  3908  iuncom4  4003  iunxiun  4078  inuni  4272  unidif0  4285  bnd2  4291  otth2  4362  copsexg  4365  copsex4g  4368  opeqsn  4374  opelopabsbALT  4382  elpwpwel  4601  suc11g  4684  rabxp  4792  opeliunxp  4810  xpundir  4812  xpiundi  4813  xpiundir  4814  brinxp2  4822  rexiunxp  4902  brres  5049  brresg  5051  dmres  5064  resiexg  5088  dminss  5182  imainss  5183  ssrnres  5210  elxp4  5255  elxp5  5256  cnvresima  5257  coundi  5269  resco  5272  imaco  5273  coiun  5277  coi1  5283  coass  5286  xpcom  5314  dffun2  5367  fncnv  5427  imadiflem  5440  imadif  5441  imainlem  5442  mptun  5495  fcnvres  5555  dff1o2  5624  dff1o3  5625  ffoss  5652  f11o  5653  brprcneu  5668  fvun2  5749  eqfnfv3  5782  respreima  5810  f1ompt  5833  fsn  5854  abrexco  5938  imaiun  5939  f1mpt  5950  dff1o6  5955  oprabid  6090  dfoprab2  6108  oprab4  6132  mpomptx  6152  opabex3d  6323  opabex3  6324  abexssex  6327  dfopab2  6396  dfoprab3s  6397  1stconst  6430  2ndconst  6431  xporderlem  6440  spc2ed  6442  f1od2  6444  brtpos2  6495  tpostpos  6508  tposmpo  6525  oviec  6888  mapsncnv  6943  dfixp  6948  domen  7001  mapsnen  7066  xpsnen  7085  xpcomco  7090  xpassen  7094  sspw1or2  7508  ltexpi  7668  dfmq0qs  7760  dfplq0qs  7761  enq0enq  7762  enq0ref  7764  enq0tr  7765  nqnq0pi  7769  prnmaxl  7819  prnminu  7820  suplocexprlemloc  8052  addsrpr  8076  mulsrpr  8077  suplocsrlemb  8137  addcnsr  8165  mulcnsr  8166  ltresr  8170  addvalex  8175  axprecex  8211  elnnz  9604  fnn0ind  9712  rexuz2  9931  qreccl  9992  rexrp  10027  elixx3g  10253  elfz2  10368  elfzuzb  10372  fznn  10445  elfz2nn0  10468  fznn0  10469  4fvwrd4  10496  elfzo2  10506  fzind2  10607  sseqn  11228  cvg1nlemres  11695  fsum2dlemstep  12145  modfsummod  12169  fprodseq  12294  divalgb  12636  bezoutlemmain  12719  isprm2  12839  oddpwdc  12896  ballotfilemelo  13166  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  xpscf  13611  issubg3  13945  releqgg  13973  eqgex  13974  imasabl  14089  prdsex  14114  prdsval  14115  prdsbaslemss  14116  dfrhm2  14399  drngprop  14555  ntreq0  15123  cnnei  15223  txlm  15270  blres  15425  isms2  15445  dedekindicclemicc  15623  limcrcl  15649  lgsquadlem1  16076  lgsquadlem2  16077  isclwwlknx  16537  clwwlknonel  16553  clwwlknon2x  16556  iseupthf1o  16569  bdcriota  16779  bj-peano4  16851  alsconv  16992