Theorem anbi1i 453

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

Syntax hints:   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi2ci  454  anbi12i  455  an12  550  anandi  579  pm5.53  791  pm5.75  946  3ancoma  969  3ioran  977  an6  1299  19.26-3an  1459  19.28h  1541  19.28  1542  eeeanv  1903  sb3an  1929  moanim  2071  nfrexdya  2468  r19.26-3  2560  r19.41  2584  rexcomf  2591  3reeanv  2599  cbvreu  2650  ceqsex3v  2723  rexab  2841  rexrab  2842  rmo4  2872  rmo3f  2876  reuind  2884  sbc3an  2965  rmo3  2995  ssrab  3170  rexun  3251  elin3  3262  inass  3281  unssdif  3306  indifdir  3327  difin2  3333  inrab2  3344  rabun2  3350  reuun2  3354  undif4  3420  rexsns  3558  rexdifsn  3650  2ralunsn  3720  iuncom4  3815  iunxiun  3889  inuni  4075  unidif0  4086  bnd2  4092  otth2  4158  copsexg  4161  copsex4g  4164  opeqsn  4169  opelopabsbALT  4176  elpwpwel  4391  suc11g  4467  rabxp  4571  opeliunxp  4589  xpundir  4591  xpiundi  4592  xpiundir  4593  brinxp2  4601  rexiunxp  4676  brres  4820  brresg  4822  dmres  4835  resiexg  4859  dminss  4948  imainss  4949  ssrnres  4976  elxp4  5021  elxp5  5022  cnvresima  5023  coundi  5035  resco  5038  imaco  5039  coiun  5043  coi1  5049  coass  5052  xpcom  5080  dffun2  5128  fncnv  5184  imadiflem  5197  imadif  5198  imainlem  5199  mptun  5249  fcnvres  5301  dff1o2  5365  dff1o3  5366  ffoss  5392  f11o  5393  brprcneu  5407  fvun2  5481  eqfnfv3  5513  respreima  5541  f1ompt  5564  fsn  5585  abrexco  5653  imaiun  5654  f1mpt  5665  dff1o6  5670  oprabid  5796  dfoprab2  5811  oprab4  5835  mpomptx  5855  opabex3d  6012  opabex3  6013  abexssex  6016  dfopab2  6080  dfoprab3s  6081  1stconst  6111  2ndconst  6112  xporderlem  6121  spc2ed  6123  f1od2  6125  brtpos2  6141  tpostpos  6154  tposmpo  6171  oviec  6528  mapsncnv  6582  dfixp  6587  domen  6638  mapsnen  6698  xpsnen  6708  xpcomco  6713  xpassen  6717  ltexpi  7138  dfmq0qs  7230  dfplq0qs  7231  enq0enq  7232  enq0ref  7234  enq0tr  7235  nqnq0pi  7239  prnmaxl  7289  prnminu  7290  suplocexprlemloc  7522  addsrpr  7546  mulsrpr  7547  suplocsrlemb  7607  addcnsr  7635  mulcnsr  7636  ltresr  7640  addvalex  7645  axprecex  7681  elnnz  9057  fnn0ind  9160  rexuz2  9369  qreccl  9427  rexrp  9457  elixx3g  9677  elfz2  9790  elfzuzb  9793  fznn  9862  elfz2nn0  9885  fznn0  9886  4fvwrd4  9910  elfzo2  9920  fzind2  10009  cvg1nlemres  10750  fsum2dlemstep  11196  modfsummod  11220  divalgb  11611  bezoutlemmain  11675  isprm2  11787  oddpwdc  11841  ntreq0  12290  cnnei  12390  txlm  12437  blres  12592  isms2  12612  dedekindicclemicc  12768  limcrcl  12785  bdcriota  13070  bj-peano4  13142  alsconv  13235