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  563  anandi  594  pm5.53  809  pm5.75  970  3ancoma  1011  3ioran  1019  an6  1357  19.26-3an  1531  19.28h  1610  19.28  1611  eeeanv  1986  sb3an  2011  moanim  2154  nfrexdya  2568  r19.26-3  2663  r19.41  2688  rexcomf  2695  3reeanv  2704  cbvreu  2765  ceqsex3v  2846  rexab  2968  rexrab  2969  rmo4  2999  rmo3f  3003  reuind  3011  sbc3an  3093  rmo3  3124  ssrab  3305  rexun  3387  elin3  3398  inass  3417  unssdif  3442  indifdir  3463  difin2  3469  inrab2  3480  rabun2  3486  reuun2  3490  undif4  3557  rexdifpr  3697  rexsns  3708  rexdifsn  3805  2ralunsn  3882  iuncom4  3977  iunxiun  4052  inuni  4245  unidif0  4257  bnd2  4263  otth2  4333  copsexg  4336  copsex4g  4339  opeqsn  4345  opelopabsbALT  4353  elpwpwel  4572  suc11g  4655  rabxp  4763  opeliunxp  4781  xpundir  4783  xpiundi  4784  xpiundir  4785  brinxp2  4793  rexiunxp  4872  brres  5019  brresg  5021  dmres  5034  resiexg  5058  dminss  5151  imainss  5152  ssrnres  5179  elxp4  5224  elxp5  5225  cnvresima  5226  coundi  5238  resco  5241  imaco  5242  coiun  5246  coi1  5252  coass  5255  xpcom  5283  dffun2  5336  fncnv  5396  imadiflem  5409  imadif  5410  imainlem  5411  mptun  5464  fcnvres  5520  dff1o2  5588  dff1o3  5589  ffoss  5616  f11o  5617  brprcneu  5632  fvun2  5713  eqfnfv3  5746  respreima  5775  f1ompt  5798  fsn  5819  abrexco  5899  imaiun  5900  f1mpt  5911  dff1o6  5916  oprabid  6049  dfoprab2  6067  oprab4  6091  mpomptx  6111  opabex3d  6282  opabex3  6283  abexssex  6286  dfopab2  6351  dfoprab3s  6352  1stconst  6385  2ndconst  6386  xporderlem  6395  spc2ed  6397  f1od2  6399  brtpos2  6416  tpostpos  6429  tposmpo  6446  oviec  6809  mapsncnv  6863  dfixp  6868  domen  6921  mapsnen  6985  xpsnen  7004  xpcomco  7009  xpassen  7013  sspw1or2  7402  ltexpi  7556  dfmq0qs  7648  dfplq0qs  7649  enq0enq  7650  enq0ref  7652  enq0tr  7653  nqnq0pi  7657  prnmaxl  7707  prnminu  7708  suplocexprlemloc  7940  addsrpr  7964  mulsrpr  7965  suplocsrlemb  8025  addcnsr  8053  mulcnsr  8054  ltresr  8058  addvalex  8063  axprecex  8099  elnnz  9488  fnn0ind  9595  rexuz2  9814  qreccl  9875  rexrp  9910  elixx3g  10135  elfz2  10249  elfzuzb  10253  fznn  10323  elfz2nn0  10346  fznn0  10347  4fvwrd4  10374  elfzo2  10384  fzind2  10484  cvg1nlemres  11545  fsum2dlemstep  11994  modfsummod  12018  fprodseq  12143  divalgb  12485  bezoutlemmain  12568  isprm2  12688  oddpwdc  12745  prdsex  13351  prdsval  13355  prdsbaslemss  13356  xpscf  13429  issubg3  13778  releqgg  13806  eqgex  13807  imasabl  13922  dfrhm2  14167  ntreq0  14855  cnnei  14955  txlm  15002  blres  15157  isms2  15177  dedekindicclemicc  15355  limcrcl  15381  lgsquadlem1  15805  lgsquadlem2  15806  isclwwlknx  16266  clwwlknonel  16282  clwwlknon2x  16285  iseupthf1o  16298  bdcriota  16478  bj-peano4  16550  alsconv  16691