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  1332  19.26-3an  1497  19.28h  1576  19.28  1577  eeeanv  1952  sb3an  1977  moanim  2119  nfrexdya  2533  r19.26-3  2627  r19.41  2652  rexcomf  2659  3reeanv  2668  cbvreu  2727  ceqsex3v  2806  rexab  2926  rexrab  2927  rmo4  2957  rmo3f  2961  reuind  2969  sbc3an  3051  rmo3  3081  ssrab  3261  rexun  3343  elin3  3354  inass  3373  unssdif  3398  indifdir  3419  difin2  3425  inrab2  3436  rabun2  3442  reuun2  3446  undif4  3513  rexdifpr  3650  rexsns  3661  rexdifsn  3754  2ralunsn  3828  iuncom4  3923  iunxiun  3998  inuni  4188  unidif0  4200  bnd2  4206  otth2  4274  copsexg  4277  copsex4g  4280  opeqsn  4285  opelopabsbALT  4293  elpwpwel  4510  suc11g  4593  rabxp  4700  opeliunxp  4718  xpundir  4720  xpiundi  4721  xpiundir  4722  brinxp2  4730  rexiunxp  4808  brres  4952  brresg  4954  dmres  4967  resiexg  4991  dminss  5084  imainss  5085  ssrnres  5112  elxp4  5157  elxp5  5158  cnvresima  5159  coundi  5171  resco  5174  imaco  5175  coiun  5179  coi1  5185  coass  5188  xpcom  5216  dffun2  5268  fncnv  5324  imadiflem  5337  imadif  5338  imainlem  5339  mptun  5389  fcnvres  5441  dff1o2  5509  dff1o3  5510  ffoss  5536  f11o  5537  brprcneu  5551  fvun2  5628  eqfnfv3  5661  respreima  5690  f1ompt  5713  fsn  5734  abrexco  5806  imaiun  5807  f1mpt  5818  dff1o6  5823  oprabid  5954  dfoprab2  5969  oprab4  5993  mpomptx  6013  opabex3d  6178  opabex3  6179  abexssex  6182  dfopab2  6247  dfoprab3s  6248  1stconst  6279  2ndconst  6280  xporderlem  6289  spc2ed  6291  f1od2  6293  brtpos2  6309  tpostpos  6322  tposmpo  6339  oviec  6700  mapsncnv  6754  dfixp  6759  domen  6810  mapsnen  6870  xpsnen  6880  xpcomco  6885  xpassen  6889  ltexpi  7404  dfmq0qs  7496  dfplq0qs  7497  enq0enq  7498  enq0ref  7500  enq0tr  7501  nqnq0pi  7505  prnmaxl  7555  prnminu  7556  suplocexprlemloc  7788  addsrpr  7812  mulsrpr  7813  suplocsrlemb  7873  addcnsr  7901  mulcnsr  7902  ltresr  7906  addvalex  7911  axprecex  7947  elnnz  9336  fnn0ind  9442  rexuz2  9655  qreccl  9716  rexrp  9751  elixx3g  9976  elfz2  10090  elfzuzb  10094  fznn  10164  elfz2nn0  10187  fznn0  10188  4fvwrd4  10215  elfzo2  10225  fzind2  10315  cvg1nlemres  11150  fsum2dlemstep  11599  modfsummod  11623  fprodseq  11748  divalgb  12090  bezoutlemmain  12165  isprm2  12285  oddpwdc  12342  prdsex  12940  xpscf  12990  issubg3  13322  releqgg  13350  eqgex  13351  imasabl  13466  dfrhm2  13710  ntreq0  14368  cnnei  14468  txlm  14515  blres  14670  isms2  14690  dedekindicclemicc  14868  limcrcl  14894  lgsquadlem1  15318  lgsquadlem2  15319  bdcriota  15529  bj-peano4  15601  alsconv  15724