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  5911  ffnov  6125  eqfnov  6128  foov  6169  opabex3d  6283  opabex3  6284  uchoice  6300  mpoxopovel  6407  tpostpos  6430  dfsmo2  6453  tfr1onlemaccex  6514  tfrcllembxssdm  6522  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  erinxp  6778  mapsncnv  6864  cbvixp  6884  ixpin  6892  ixpiinm  6893  mptelixpg  6903  elixpsn  6904  ixpsnf1o  6905  mapsnen  6986  xpassen  7014  2omotaplemap  7476  distrnqg  7607  subhalfnqq  7634  enq0enq  7651  enq0sym  7652  enq0tr  7654  addnq0mo  7667  mulnq0mo  7668  distrnq0  7679  prarloc  7723  nqprrnd  7763  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemdisj  7826  ltexprlemloc  7827  recexprlemdisj  7850  caucvgprprlemell  7905  caucvgprprlemelu  7906  addsrmo  7963  mulsrmo  7964  opelreal  8047  axcaucvglemres  8119  axpre-suploc  8122  elnnz  9489  elznn0nn  9493  zltlen  9558  suprzclex  9578  peano2uz2  9587  peano5uzti  9588  qltlen  9874  elfzuzb  10254  4fvwrd4  10375  fzind2  10486  cvg1nlemres  11563  rexfiuz  11567  cbvsum  11938  mertenslem2  12115  mertensabs  12116  cbvprod  12137  prodmodc  12157  fprodseq  12162  ndvdssub  12509  bitsmod  12535  nnwosdc  12628  isprm2  12707  isprm4  12709  hashdvds  12811  xpscf  13448  fngsum  13489  igsumvalx  13490  isnsg2  13808  isnsg4  13817  isrhm  14191  issubrng  14232  subsubrng2  14248  subsubrg2  14279  isbasis2g  14788  tgval2  14794  elcncf1di  15322  dedekindicclemicc  15375  dedekindicc  15376  plyco  15502  isclwwlk  16264  clwwlknon2x  16305  iseupthf1o  16318  2omap  16645