Theorem anbi1i 439

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

Syntax hints:   ∧ wa 101   ↔ wb 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105

This theorem depends on definitions:  df-bi 114

This theorem is referenced by:  anbi2ci  440  anbi12i  441  an12  503  anandi  532  pm5.53  726  pm5.75  880  3ancoma  903  3ioran  911  an6  1227  19.26-3an  1388  19.28h  1470  19.28  1471  eeeanv  1824  sb3an  1848  moanim  1990  nfrexdya  2376  r19.26-3  2460  r19.41  2482  rexcomf  2489  3reeanv  2497  cbvreu  2548  ceqsex3v  2613  rexab  2725  rexrab  2726  rmo4  2756  reuind  2766  sbc3an  2846  rmo3  2876  ssrab  3045  rexun  3150  elin3  3155  inass  3174  unssdif  3199  indifdir  3220  difin2  3226  inrab2  3237  rabun2  3243  reuun2  3247  undif4  3311  rexsns  3436  rexsnsOLD  3437  rexdifsn  3526  2ralunsn  3596  iuncom4  3691  iunxiun  3763  inuni  3936  unidif0  3947  bnd2  3953  otth2  4005  copsexg  4008  copsex4g  4011  opeqsn  4016  opelopabsbALT  4023  suc11g  4308  rabxp  4407  opeliunxp  4422  xpundir  4424  xpiundi  4425  xpiundir  4426  brinxp2  4434  rexiunxp  4505  brres  4645  brresg  4647  dmres  4659  resiexg  4680  dminss  4765  imainss  4766  ssrnres  4790  elxp4  4835  elxp5  4836  cnvresima  4837  coundi  4849  resco  4852  imaco  4853  coiun  4857  coi1  4863  coass  4866  xpcom  4891  dffun2  4939  fncnv  4992  imadiflem  5005  imadif  5006  imainlem  5007  mptun  5056  fcnvres  5100  dff1o2  5158  dff1o3  5159  ffoss  5185  f11o  5186  brprcneu  5198  fvun2  5267  eqfnfv3  5294  respreima  5322  f1ompt  5347  fsn  5362  abrexco  5425  imaiun  5426  f1mpt  5437  dff1o6  5443  oprabid  5564  dfoprab2  5579  oprab4  5602  mpt2mptx  5622  opabex3d  5775  opabex3  5776  abexssex  5779  dfopab2  5842  dfoprab3s  5843  1stconst  5869  2ndconst  5870  xporderlem  5879  spc2ed  5881  f1od2  5883  brtpos2  5896  tpostpos  5909  tposmpt2  5926  oviec  6242  domen  6262  xpsnen  6325  xpcomco  6330  xpassen  6334  ltexpi  6492  dfmq0qs  6584  dfplq0qs  6585  enq0enq  6586  enq0ref  6588  enq0tr  6589  nqnq0pi  6593  prnmaxl  6643  prnminu  6644  addsrpr  6887  mulsrpr  6888  addcnsr  6967  mulcnsr  6968  ltresr  6972  addvalex  6977  axprecex  7011  elnnz  8311  fnn0ind  8412  rexuz2  8619  qreccl  8673  rexrp  8702  elixx3g  8870  elfz2  8982  elfzuzb  8985  fznn  9052  elfz2nn0  9074  fznn0  9075  4fvwrd4  9098  elfzo2  9108  fzind2  9196  cvg1nlemres  9811  oddpwdc  10241  bdcriota  10369  bj-peano4  10446  alsconv  10485