Theorem anbi2i 457

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 454	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:  anbi12i  460  bianass  469  mpan10  474  an4  588  an42  589  anandir  595  dcim  848  19.27h  1608  19.27  1609  19.41  1734  sbcof2  1858  sbidm  1899  sb6  1935  3exdistr  1964  4exdistr  1965  2sb5  2036  2sb5rf  2042  sbel2x  2051  eu2  2124  euan  2136  sbmo  2139  mo4f  2140  eu4  2142  moanim  2154  2eu4  2173  clelab  2357  nonconne  2414  r2exf  2550  ceqsex3v  2846  ceqsex4v  2847  ceqsex8v  2849  reu2  2994  reu6  2995  reu4  3000  reu7  3001  rmo3f  3003  rmo4f  3004  2rmorex  3012  rmo3  3124  raldifb  3347  inass  3417  dfss4st  3440  ssddif  3441  difin  3444  invdif  3449  indif  3450  indi  3454  difundi  3459  difindiss  3461  inssdif0im  3562  rexdifpr  3697  ssdifsn  3801  unipr  3907  uniun  3912  uniin  3913  iunin2  4034  iindif2m  4038  iinin2m  4039  elpwpw  4057  unidif0  4257  mss  4318  eqvinop  4335  opcom  4343  opeqsn  4345  uniuni  4548  zfinf2  4687  elomssom  4703  fconstmpt  4773  opeliunxp  4781  xpundi  4782  elvvv  4789  xpiindim  4867  elcnv2  4908  cnvuni  4916  dmuni  4941  opelres  5018  restidsing  5069  elima3  5083  imai  5092  imainss  5152  ssrnres  5179  cnvresima  5226  mptpreima  5230  coundir  5239  rnco  5243  coass  5255  relrelss  5263  dffun2  5336  dffun4  5337  dffun6f  5339  dffun4f  5342  dffun7  5353  dffun8  5354  dffun9  5355  svrelfun  5395  fncnv  5396  funcnvuni  5399  dfmpt3  5455  fintm  5522  fin  5523  dff12  5541  fores  5569  dff1o4  5591  eqfnfv3  5746  unpreima  5772  ffnfvf  5806  dff13f  5910  ffnov  6124  eqfnov  6127  foov  6168  opabex3d  6282  opabex3  6283  uchoice  6299  mpoxopovel  6406  tpostpos  6429  dfsmo2  6452  tfr1onlemaccex  6513  tfrcllembxssdm  6521  tfrcllemaccex  6526  tfrcllemres  6527  tfrcldm  6528  erinxp  6777  mapsncnv  6863  cbvixp  6883  ixpin  6891  ixpiinm  6892  mptelixpg  6902  elixpsn  6903  ixpsnf1o  6904  mapsnen  6985  xpassen  7013  2omotaplemap  7475  distrnqg  7606  subhalfnqq  7633  enq0enq  7650  enq0sym  7651  enq0tr  7653  addnq0mo  7666  mulnq0mo  7667  distrnq0  7678  prarloc  7722  nqprrnd  7762  ltexprlemopl  7820  ltexprlemlol  7821  ltexprlemopu  7822  ltexprlemupu  7823  ltexprlemdisj  7825  ltexprlemloc  7826  recexprlemdisj  7849  caucvgprprlemell  7904  caucvgprprlemelu  7905  addsrmo  7962  mulsrmo  7963  opelreal  8046  axcaucvglemres  8118  axpre-suploc  8121  elnnz  9488  elznn0nn  9492  zltlen  9557  suprzclex  9577  peano2uz2  9586  peano5uzti  9587  qltlen  9873  elfzuzb  10253  4fvwrd4  10374  fzind2  10484  cvg1nlemres  11545  rexfiuz  11549  cbvsum  11920  mertenslem2  12096  mertensabs  12097  cbvprod  12118  prodmodc  12138  fprodseq  12143  ndvdssub  12490  bitsmod  12516  nnwosdc  12609  isprm2  12688  isprm4  12690  hashdvds  12792  xpscf  13429  fngsum  13470  igsumvalx  13471  isnsg2  13789  isnsg4  13798  isrhm  14171  issubrng  14212  subsubrng2  14228  subsubrg2  14259  isbasis2g  14768  tgval2  14774  elcncf1di  15302  dedekindicclemicc  15355  dedekindicc  15356  plyco  15482  isclwwlk  16244  clwwlknon2x  16285  iseupthf1o  16298  2omap  16594