Theorem anbi1i 462

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 459	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  463  anbi12i  464  bianassc  474  an12  567  anandi  598  pm5.53  814  pm5.75  975  3ancoma  1016  3ioran  1024  an6  1362  19.26-3an  1536  19.28h  1615  19.28  1616  eeeanv  1993  sb3an  2018  moanim  2161  nfrexdya  2586  r19.26-3  2681  r19.41  2706  rexcomf  2713  3reeanv  2722  cbvreu  2784  ceqsex3v  2865  rexab  2988  rexrab  2989  rmo4  3019  rmo3f  3023  reuind  3031  sbc3an  3113  rmo3  3144  ssrab  3326  rexun  3409  elin3  3420  inass  3441  unssdif  3466  indifdir  3487  difin2  3493  inrab2  3506  rabun2  3512  reuun2  3516  undif4  3586  rexdifpr  3733  rexsns  3744  rexdifsn  3841  2ralunsn  3919  iuncom4  4014  iunxiun  4089  inuni  4286  unidif0  4299  bnd2  4305  otth2  4376  copsexg  4379  copsex4g  4382  opeqsn  4388  opelopabsbALT  4396  elpwpwel  4616  suc11g  4699  rabxp  4807  opeliunxp  4825  xpundir  4827  xpiundi  4828  xpiundir  4829  brinxp2  4837  rexiunxp  4917  brres  5064  brresg  5066  dmres  5079  resiexg  5103  dminss  5197  imainss  5198  ssrnres  5225  elxp4  5270  elxp5  5271  cnvresima  5272  coundi  5284  resco  5287  imaco  5288  coiun  5292  coi1  5298  coass  5301  xpcom  5329  dffun2  5382  fncnv  5442  imadiflem  5455  imadif  5456  imainlem  5457  mptun  5510  fcnvres  5570  dff1o2  5639  dff1o3  5640  ffoss  5667  f11o  5668  brprcneu  5683  fvun2  5764  eqfnfv3  5799  respreima  5827  f1ompt  5850  fsn  5871  abrexco  5955  imaiun  5956  f1mpt  5967  dff1o6  5972  oprabid  6107  dfoprab2  6125  oprab4  6149  mpomptx  6169  opabex3d  6340  opabex3  6341  abexssex  6344  dfopab2  6413  dfoprab3s  6414  1stconst  6447  2ndconst  6448  xporderlem  6457  spc2ed  6459  f1od2  6461  brtpos2  6512  tpostpos  6525  tposmpo  6542  oviec  6905  mapsncnv  6967  dfixp  6972  domen  7025  mapsnen  7090  xpsnen  7109  xpcomco  7114  xpassen  7118  sspw1or2  7534  ltexpi  7694  dfmq0qs  7786  dfplq0qs  7787  enq0enq  7788  enq0ref  7790  enq0tr  7791  nqnq0pi  7795  prnmaxl  7845  prnminu  7846  suplocexprlemloc  8078  addsrpr  8102  mulsrpr  8103  suplocsrlemb  8163  addcnsr  8191  mulcnsr  8192  ltresr  8196  addvalex  8201  axprecex  8237  elnnz  9633  fnn0ind  9741  rexuz2  9960  qreccl  10021  rexrp  10056  elixx3g  10282  elfz2  10397  elfzuzb  10401  fznn  10474  elfz2nn0  10497  fznn0  10498  4fvwrd4  10525  elfzo2  10535  fzind2  10636  sseqn  11257  hashf1lem1  11263  hashf1lem2  11264  cvg1nlemres  11729  fsum2dlemstep  12179  modfsummod  12203  fprodseq  12328  divalgb  12670  bezoutlemmain  12753  isprm2  12873  oddpwdc  12930  ballotfilemelo  13200  ballotfilem2  13206  ballotfilemfc0  13210  ballotfilemfcc  13211  xpscf  13645  issubg3  13972  releqgg  14000  eqgex  14001  imasabl  14117  prdsex  14149  prdsval  14150  prdsbaslemss  14151  dfrhm2  14434  drngprop  14590  ntreq0  15156  cnnei  15256  txlm  15303  blres  15458  isms2  15478  dedekindicclemicc  15656  limcrcl  15682  lgsquadlem1  16110  lgsquadlem2  16111  isclwwlknx  16571  clwwlknonel  16587  clwwlknon2x  16590  iseupthf1o  16603  bdcriota  16823  bj-peano4  16895  alsconv  17035