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  590  pm5.53  803  pm5.75  964  3ancoma  987  3ioran  995  an6  1333  19.26-3an  1505  19.28h  1584  19.28  1585  eeeanv  1960  sb3an  1985  moanim  2127  nfrexdya  2541  r19.26-3  2635  r19.41  2660  rexcomf  2667  3reeanv  2676  cbvreu  2735  ceqsex3v  2814  rexab  2934  rexrab  2935  rmo4  2965  rmo3f  2969  reuind  2977  sbc3an  3059  rmo3  3089  ssrab  3270  rexun  3352  elin3  3363  inass  3382  unssdif  3407  indifdir  3428  difin2  3434  inrab2  3445  rabun2  3451  reuun2  3455  undif4  3522  rexdifpr  3660  rexsns  3671  rexdifsn  3764  2ralunsn  3838  iuncom4  3933  iunxiun  4008  inuni  4198  unidif0  4210  bnd2  4216  otth2  4284  copsexg  4287  copsex4g  4290  opeqsn  4296  opelopabsbALT  4304  elpwpwel  4521  suc11g  4604  rabxp  4711  opeliunxp  4729  xpundir  4731  xpiundi  4732  xpiundir  4733  brinxp2  4741  rexiunxp  4819  brres  4964  brresg  4966  dmres  4979  resiexg  5003  dminss  5096  imainss  5097  ssrnres  5124  elxp4  5169  elxp5  5170  cnvresima  5171  coundi  5183  resco  5186  imaco  5187  coiun  5191  coi1  5197  coass  5200  xpcom  5228  dffun2  5280  fncnv  5339  imadiflem  5352  imadif  5353  imainlem  5354  mptun  5406  fcnvres  5458  dff1o2  5526  dff1o3  5527  ffoss  5553  f11o  5554  brprcneu  5568  fvun2  5645  eqfnfv3  5678  respreima  5707  f1ompt  5730  fsn  5751  abrexco  5827  imaiun  5828  f1mpt  5839  dff1o6  5844  oprabid  5975  dfoprab2  5991  oprab4  6015  mpomptx  6035  opabex3d  6205  opabex3  6206  abexssex  6209  dfopab2  6274  dfoprab3s  6275  1stconst  6306  2ndconst  6307  xporderlem  6316  spc2ed  6318  f1od2  6320  brtpos2  6336  tpostpos  6349  tposmpo  6366  oviec  6727  mapsncnv  6781  dfixp  6786  domen  6839  mapsnen  6902  xpsnen  6915  xpcomco  6920  xpassen  6924  ltexpi  7449  dfmq0qs  7541  dfplq0qs  7542  enq0enq  7543  enq0ref  7545  enq0tr  7546  nqnq0pi  7550  prnmaxl  7600  prnminu  7601  suplocexprlemloc  7833  addsrpr  7857  mulsrpr  7858  suplocsrlemb  7918  addcnsr  7946  mulcnsr  7947  ltresr  7951  addvalex  7956  axprecex  7992  elnnz  9381  fnn0ind  9488  rexuz2  9701  qreccl  9762  rexrp  9797  elixx3g  10022  elfz2  10136  elfzuzb  10140  fznn  10210  elfz2nn0  10233  fznn0  10234  4fvwrd4  10261  elfzo2  10271  fzind2  10366  cvg1nlemres  11238  fsum2dlemstep  11687  modfsummod  11711  fprodseq  11836  divalgb  12178  bezoutlemmain  12261  isprm2  12381  oddpwdc  12438  prdsex  13043  prdsval  13047  prdsbaslemss  13048  xpscf  13121  issubg3  13470  releqgg  13498  eqgex  13499  imasabl  13614  dfrhm2  13858  ntreq0  14546  cnnei  14646  txlm  14693  blres  14848  isms2  14868  dedekindicclemicc  15046  limcrcl  15072  lgsquadlem1  15496  lgsquadlem2  15497  bdcriota  15752  bj-peano4  15824  alsconv  15952