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  4295  opelopabsbALT  4303  elpwpwel  4520  suc11g  4603  rabxp  4710  opeliunxp  4728  xpundir  4730  xpiundi  4731  xpiundir  4732  brinxp2  4740  rexiunxp  4818  brres  4962  brresg  4964  dmres  4977  resiexg  5001  dminss  5094  imainss  5095  ssrnres  5122  elxp4  5167  elxp5  5168  cnvresima  5169  coundi  5181  resco  5184  imaco  5185  coiun  5189  coi1  5195  coass  5198  xpcom  5226  dffun2  5278  fncnv  5334  imadiflem  5347  imadif  5348  imainlem  5349  mptun  5401  fcnvres  5453  dff1o2  5521  dff1o3  5522  ffoss  5548  f11o  5549  brprcneu  5563  fvun2  5640  eqfnfv3  5673  respreima  5702  f1ompt  5725  fsn  5746  abrexco  5818  imaiun  5819  f1mpt  5830  dff1o6  5835  oprabid  5966  dfoprab2  5982  oprab4  6006  mpomptx  6026  opabex3d  6196  opabex3  6197  abexssex  6200  dfopab2  6265  dfoprab3s  6266  1stconst  6297  2ndconst  6298  xporderlem  6307  spc2ed  6309  f1od2  6311  brtpos2  6327  tpostpos  6340  tposmpo  6357  oviec  6718  mapsncnv  6772  dfixp  6777  domen  6828  mapsnen  6888  xpsnen  6898  xpcomco  6903  xpassen  6907  ltexpi  7432  dfmq0qs  7524  dfplq0qs  7525  enq0enq  7526  enq0ref  7528  enq0tr  7529  nqnq0pi  7533  prnmaxl  7583  prnminu  7584  suplocexprlemloc  7816  addsrpr  7840  mulsrpr  7841  suplocsrlemb  7901  addcnsr  7929  mulcnsr  7930  ltresr  7934  addvalex  7939  axprecex  7975  elnnz  9364  fnn0ind  9471  rexuz2  9684  qreccl  9745  rexrp  9780  elixx3g  10005  elfz2  10119  elfzuzb  10123  fznn  10193  elfz2nn0  10216  fznn0  10217  4fvwrd4  10244  elfzo2  10254  fzind2  10349  cvg1nlemres  11215  fsum2dlemstep  11664  modfsummod  11688  fprodseq  11813  divalgb  12155  bezoutlemmain  12238  isprm2  12358  oddpwdc  12415  prdsex  13019  prdsval  13023  prdsbaslemss  13024  xpscf  13097  issubg3  13446  releqgg  13474  eqgex  13475  imasabl  13590  dfrhm2  13834  ntreq0  14522  cnnei  14622  txlm  14669  blres  14824  isms2  14844  dedekindicclemicc  15022  limcrcl  15048  lgsquadlem1  15472  lgsquadlem2  15473  bdcriota  15683  bj-peano4  15755  alsconv  15883