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 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3587  rexdifpr  3737  rexsns  3748  rexdifsn  3846  2ralunsn  3924  iuncom4  4019  iunxiun  4094  inuni  4293  unidif0  4306  bnd2  4312  otth2  4383  copsexg  4386  copsex4g  4389  opeqsn  4395  opelopabsbALT  4403  elpwpwel  4623  suc11g  4706  rabxp  4814  opeliunxp  4832  xpundir  4834  xpiundi  4835  xpiundir  4836  brinxp2  4844  rexiunxp  4924  brres  5071  brresg  5073  dmres  5086  resiexg  5111  dminss  5205  imainss  5206  ssrnres  5233  elxp4  5278  elxp5  5279  cnvresima  5280  coundi  5292  resco  5295  imaco  5296  coiun  5300  coi1  5306  coass  5309  xpcom  5337  dffun2  5390  fncnv  5450  imadiflem  5463  imadif  5464  imainlem  5465  mptun  5518  fcnvres  5578  dff1o2  5647  dff1o3  5648  ffoss  5675  f11o  5676  brprcneu  5691  fvun2  5773  eqfnfv3  5811  respreima  5839  f1ompt  5862  fsn  5883  abrexco  5968  imaiun  5969  f1mpt  5980  dff1o6  5985  oprabid  6120  dfoprab2  6138  oprab4  6162  mpomptx  6182  opabex3d  6354  opabex3  6355  abexssex  6358  dfopab2  6427  dfoprab3s  6428  1stconst  6461  2ndconst  6462  xporderlem  6471  spc2ed  6473  f1od2  6475  brtpos2  6526  tpostpos  6539  tposmpo  6556  oviec  6919  mapsncnv  6981  dfixp  6986  domen  7039  mapsnen  7104  xpsnen  7123  xpcomco  7128  xpassen  7132  sspw1or2  7550  ltexpi  7710  dfmq0qs  7802  dfplq0qs  7803  enq0enq  7804  enq0ref  7806  enq0tr  7807  nqnq0pi  7811  prnmaxl  7861  prnminu  7862  suplocexprlemloc  8094  addsrpr  8118  mulsrpr  8119  suplocsrlemb  8179  addcnsr  8207  mulcnsr  8208  ltresr  8212  addvalex  8217  axprecex  8253  elnnz  9665  fnn0ind  9773  rexuz2  9997  qreccl  10058  rexrp  10094  elixx3g  10320  elfz2  10435  elfzuzb  10439  fznn  10513  elfz2nn0  10536  fznn0  10537  4fvwrd4  10564  elfzo2  10574  fzind2  10675  sseqn  11301  hashf1lem1  11307  hashf1lem2  11308  cvg1nlemres  11773  fsum2dlemstep  12226  modfsummod  12250  fprodseq  12375  divalgb  12717  bezoutlemmain  12800  isprm2  12920  nnmaxpw  12978  ballotfilemelo  13280  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  xpscf  13727  issubg3  14054  releqgg  14082  eqgex  14083  imasabl  14230  prdsex  14279  prdsval  14280  prdsbaslemss  14281  dfrhm2  14570  drngprop  14726  isassa  15111  ntreq0  15358  cnnei  15458  txlm  15505  blres  15660  isms2  15680  dedekindicclemicc  15858  limcrcl  15884  lgsquadlem1  16401  lgsquadlem2  16402  isclwwlknx  16862  clwwlknonel  16878  clwwlknon2x  16881  iseupthf1o  16894  bdcriota  17114  bj-peano4  17186  alsanmo  17358  ralsanmo  17359  alsralrex  17360  alsraln0m  17361