Theorem anbi2i 461

Description: Introduce a left 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
anbi2i	⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))

Proof of Theorem anbi2i

Step	Hyp	Ref	Expression
1		bi.aa	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.32i 458	1 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi12i  464  bianass  473  mpan10  478  an4  592  an42  593  anandir  599  dcim  853  19.27h  1613  19.27  1614  19.41  1738  sbcof2  1863  sbidm  1904  sb6  1941  3exdistr  1971  4exdistr  1972  2sb5  2043  2sb5rf  2049  sbel2x  2058  eu2  2131  euan  2143  sbmo  2146  mo4f  2147  eu4  2149  moanim  2161  2eu4  2180  clelab  2366  nonconne  2432  r2exf  2568  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  reu2  3014  reu6  3015  reu4  3020  reu7  3021  rmo3f  3023  rmo4f  3024  2rmorex  3032  rmo3  3144  raldifb  3369  inass  3441  dfss4st  3464  ssddif  3465  difin  3468  invdif  3473  indif  3474  indi  3478  difundi  3483  difindiss  3485  inssdif0imOLD  3593  rexdifpr  3737  ssdifsn  3842  unipr  3949  uniun  3954  uniin  3955  iunin2  4076  iindif2m  4080  iinin2m  4081  elpwpw  4099  unidif0  4304  mss  4366  eqvinop  4383  opcom  4391  opeqsn  4393  uniuni  4597  zfinf2  4736  elomssom  4752  fconstmpt  4822  opeliunxp  4830  xpundi  4831  elvvv  4838  xpiindim  4917  elcnv2  4958  cnvuni  4966  dmuni  4991  opelres  5068  restidsing  5119  elima3  5133  imai  5143  imainss  5203  ssrnres  5230  cnvresima  5277  mptpreima  5281  coundir  5290  rnco  5294  coass  5306  relrelss  5314  dffun2  5387  dffun4  5388  dffun6f  5390  dffun4f  5393  dffun7  5404  dffun8  5405  dffun9  5406  svrelfun  5446  fncnv  5447  funcnvuni  5450  dfmpt3  5506  fintm  5577  fin  5578  dff12  5597  fores  5625  dff1o4  5647  eqfnfv3  5808  unpreima  5833  ffnfvf  5867  dff13f  5976  ffnov  6192  eqfnov  6195  foov  6236  opabex3d  6350  opabex3  6351  uchoice  6371  mpoxopovel  6512  tpostpos  6535  dfsmo2  6558  tfr1onlemaccex  6619  tfrcllembxssdm  6627  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  erinxp  6883  mapsncnv  6977  cbvixp  6997  ixpin  7005  ixpiinm  7006  mptelixpg  7016  elixpsn  7017  ixpsnf1o  7018  mapsnen  7100  xpassen  7128  2omap  7319  2omotaplemap  7624  distrnqg  7755  subhalfnqq  7782  enq0enq  7799  enq0sym  7800  enq0tr  7802  addnq0mo  7815  mulnq0mo  7816  distrnq0  7827  prarloc  7871  nqprrnd  7911  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemdisj  7974  ltexprlemloc  7975  recexprlemdisj  7998  caucvgprprlemell  8053  caucvgprprlemelu  8054  addsrmo  8111  mulsrmo  8112  opelreal  8195  axcaucvglemres  8267  axpre-suploc  8270  elnnz  9659  elznn0nn  9663  zltlen  9729  suprzclex  9749  peano2uz2  9758  peano5uzti  9759  qltlen  10050  elfzuzb  10433  4fvwrd4  10558  fzind2  10669  cvg1nlemres  11767  rexfiuz  11771  cbvsum  12145  mertenslem2  12322  mertensabs  12323  cbvprod  12344  prodmodc  12364  fprodseq  12369  ndvdssub  12716  bitsmod  12742  nnwosdc  12835  isprm2  12914  isprm4  12916  hashdvds  13022  xpscf  13721  fngzsum  13761  gzsumvalx  13762  isnsg2  14059  isnsg4  14068  isrhm  14549  issubrng  14591  subsubrng2  14607  subsubrg2  14638  psrbaglefifi  15147  isbasis2g  15237  tgval2  15243  elcncf1di  15771  dedekindicclemicc  15824  dedekindicc  15825  plyco  15951  isclwwlk  16801  clwwlknon2x  16842  iseupthf1o  16855  alsanmo  17318  ralsanmo  17319  2alsraln0m  17325  2alsraln0idm  17326