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  4306  mss  4368  eqvinop  4385  opcom  4393  opeqsn  4395  uniuni  4599  zfinf2  4738  elomssom  4754  fconstmpt  4824  opeliunxp  4832  xpundi  4833  elvvv  4840  xpiindim  4919  elcnv2  4960  cnvuni  4968  dmuni  4993  opelres  5070  restidsing  5122  elima3  5136  imai  5146  imainss  5206  ssrnres  5233  cnvresima  5280  mptpreima  5284  coundir  5293  rnco  5297  coass  5309  relrelss  5317  dffun2  5390  dffun4  5391  dffun6f  5393  dffun4f  5396  dffun7  5407  dffun8  5408  dffun9  5409  svrelfun  5449  fncnv  5450  funcnvuni  5453  dfmpt3  5509  fintm  5580  fin  5581  dff12  5600  fores  5628  dff1o4  5650  eqfnfv3  5811  unpreima  5836  ffnfvf  5870  dff13f  5979  ffnov  6195  eqfnov  6198  foov  6239  opabex3d  6354  opabex3  6355  uchoice  6375  mpoxopovel  6516  tpostpos  6539  dfsmo2  6562  tfr1onlemaccex  6623  tfrcllembxssdm  6631  tfrcllemaccex  6636  tfrcllemres  6637  tfrcldm  6638  erinxp  6887  mapsncnv  6981  cbvixp  7001  ixpin  7009  ixpiinm  7010  mptelixpg  7020  elixpsn  7021  ixpsnf1o  7022  mapsnen  7104  xpassen  7132  2omap  7324  2omotaplemap  7629  distrnqg  7760  subhalfnqq  7787  enq0enq  7804  enq0sym  7805  enq0tr  7807  addnq0mo  7820  mulnq0mo  7821  distrnq0  7832  prarloc  7876  nqprrnd  7916  ltexprlemopl  7974  ltexprlemlol  7975  ltexprlemopu  7976  ltexprlemupu  7977  ltexprlemdisj  7979  ltexprlemloc  7980  recexprlemdisj  8003  caucvgprprlemell  8058  caucvgprprlemelu  8059  addsrmo  8116  mulsrmo  8117  opelreal  8200  axcaucvglemres  8272  axpre-suploc  8275  elnnz  9665  elznn0nn  9669  zltlen  9735  suprzclex  9755  peano2uz2  9764  peano5uzti  9765  qltlen  10056  elfzuzb  10439  4fvwrd4  10564  fzind2  10675  cvg1nlemres  11773  rexfiuz  11777  cbvsum  12151  mertenslem2  12328  mertensabs  12329  cbvprod  12350  prodmodc  12370  fprodseq  12375  ndvdssub  12722  bitsmod  12748  nnwosdc  12841  isprm2  12920  isprm4  12922  hashdvds  13028  xpscf  13727  fngzsum  13767  gzsumvalx  13768  isnsg2  14065  isnsg4  14074  isrhm  14574  issubrng  14616  subsubrng2  14632  subsubrg2  14663  psrbaglefifi  15172  isbasis2g  15271  tgval2  15277  elcncf1di  15805  dedekindicclemicc  15858  dedekindicc  15859  plyco  15985  isclwwlk  16840  clwwlknon2x  16881  iseupthf1o  16894  idjudju  17252  alsanmo  17358  ralsanmo  17359  2alsraln0m  17365  2alsraln0idm  17366