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  3262  rexun  3344  elin3  3355  inass  3374  unssdif  3399  indifdir  3420  difin2  3426  inrab2  3437  rabun2  3443  reuun2  3447  undif4  3514  rexdifpr  3651  rexsns  3662  rexdifsn  3755  2ralunsn  3829  iuncom4  3924  iunxiun  3999  inuni  4189  unidif0  4201  bnd2  4207  otth2  4275  copsexg  4278  copsex4g  4281  opeqsn  4286  opelopabsbALT  4294  elpwpwel  4511  suc11g  4594  rabxp  4701  opeliunxp  4719  xpundir  4721  xpiundi  4722  xpiundir  4723  brinxp2  4731  rexiunxp  4809  brres  4953  brresg  4955  dmres  4968  resiexg  4992  dminss  5085  imainss  5086  ssrnres  5113  elxp4  5158  elxp5  5159  cnvresima  5160  coundi  5172  resco  5175  imaco  5176  coiun  5180  coi1  5186  coass  5189  xpcom  5217  dffun2  5269  fncnv  5325  imadiflem  5338  imadif  5339  imainlem  5340  mptun  5392  fcnvres  5444  dff1o2  5512  dff1o3  5513  ffoss  5539  f11o  5540  brprcneu  5554  fvun2  5631  eqfnfv3  5664  respreima  5693  f1ompt  5716  fsn  5737  abrexco  5809  imaiun  5810  f1mpt  5821  dff1o6  5826  oprabid  5957  dfoprab2  5973  oprab4  5997  mpomptx  6017  opabex3d  6187  opabex3  6188  abexssex  6191  dfopab2  6256  dfoprab3s  6257  1stconst  6288  2ndconst  6289  xporderlem  6298  spc2ed  6300  f1od2  6302  brtpos2  6318  tpostpos  6331  tposmpo  6348  oviec  6709  mapsncnv  6763  dfixp  6768  domen  6819  mapsnen  6879  xpsnen  6889  xpcomco  6894  xpassen  6898  ltexpi  7423  dfmq0qs  7515  dfplq0qs  7516  enq0enq  7517  enq0ref  7519  enq0tr  7520  nqnq0pi  7524  prnmaxl  7574  prnminu  7575  suplocexprlemloc  7807  addsrpr  7831  mulsrpr  7832  suplocsrlemb  7892  addcnsr  7920  mulcnsr  7921  ltresr  7925  addvalex  7930  axprecex  7966  elnnz  9355  fnn0ind  9461  rexuz2  9674  qreccl  9735  rexrp  9770  elixx3g  9995  elfz2  10109  elfzuzb  10113  fznn  10183  elfz2nn0  10206  fznn0  10207  4fvwrd4  10234  elfzo2  10244  fzind2  10334  cvg1nlemres  11169  fsum2dlemstep  11618  modfsummod  11642  fprodseq  11767  divalgb  12109  bezoutlemmain  12192  isprm2  12312  oddpwdc  12369  prdsex  12973  prdsval  12977  prdsbaslemss  12978  xpscf  13051  issubg3  13400  releqgg  13428  eqgex  13429  imasabl  13544  dfrhm2  13788  ntreq0  14476  cnnei  14576  txlm  14623  blres  14778  isms2  14798  dedekindicclemicc  14976  limcrcl  15002  lgsquadlem1  15426  lgsquadlem2  15427  bdcriota  15637  bj-peano4  15709  alsconv  15837