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  586  an42  587  anandir  591  dcim  841  19.27h  1560  19.27  1561  19.41  1686  sbcof2  1810  sbidm  1851  sb6  1886  3exdistr  1915  4exdistr  1916  2sb5  1983  2sb5rf  1989  sbel2x  1998  eu2  2070  euan  2082  sbmo  2085  mo4f  2086  eu4  2088  moanim  2100  2eu4  2119  clelab  2303  nonconne  2359  r2exf  2495  ceqsex3v  2779  ceqsex4v  2780  ceqsex8v  2782  reu2  2925  reu6  2926  reu4  2931  reu7  2932  rmo3f  2934  rmo4f  2935  2rmorex  2943  rmo3  3054  raldifb  3275  inass  3345  dfss4st  3368  ssddif  3369  difin  3372  invdif  3377  indif  3378  indi  3382  difundi  3387  difindiss  3389  inssdif0im  3490  rexdifpr  3619  ssdifsn  3719  unipr  3821  uniun  3826  uniin  3827  iunin2  3947  iindif2m  3951  iinin2m  3952  elpwpw  3970  unidif0  4164  mss  4222  eqvinop  4239  opcom  4246  opeqsn  4248  uniuni  4447  zfinf2  4584  elomssom  4600  fconstmpt  4669  opeliunxp  4677  xpundi  4678  elvvv  4685  xpiindim  4759  elcnv2  4800  cnvuni  4808  dmuni  4832  opelres  4907  restidsing  4958  elima3  4972  imai  4979  imainss  5039  ssrnres  5066  cnvresima  5113  mptpreima  5117  coundir  5126  rnco  5130  coass  5142  relrelss  5150  dffun2  5221  dffun4  5222  dffun6f  5224  dffun4f  5227  dffun7  5238  dffun8  5239  dffun9  5240  svrelfun  5276  fncnv  5277  funcnvuni  5280  dfmpt3  5333  fintm  5396  fin  5397  dff12  5415  fores  5442  dff1o4  5464  eqfnfv3  5610  unpreima  5636  ffnfvf  5670  dff13f  5764  ffnov  5972  eqfnov  5974  foov  6014  opabex3d  6115  opabex3  6116  mpoxopovel  6235  tpostpos  6258  dfsmo2  6281  tfr1onlemaccex  6342  tfrcllembxssdm  6350  tfrcllemaccex  6355  tfrcllemres  6356  tfrcldm  6357  erinxp  6602  mapsncnv  6688  cbvixp  6708  ixpin  6716  ixpiinm  6717  mptelixpg  6727  elixpsn  6728  ixpsnf1o  6729  mapsnen  6804  xpassen  6823  distrnqg  7364  subhalfnqq  7391  enq0enq  7408  enq0sym  7409  enq0tr  7411  addnq0mo  7424  mulnq0mo  7425  distrnq0  7436  prarloc  7480  nqprrnd  7520  ltexprlemopl  7578  ltexprlemlol  7579  ltexprlemopu  7580  ltexprlemupu  7581  ltexprlemdisj  7583  ltexprlemloc  7584  recexprlemdisj  7607  caucvgprprlemell  7662  caucvgprprlemelu  7663  addsrmo  7720  mulsrmo  7721  opelreal  7804  axcaucvglemres  7876  axpre-suploc  7879  elnnz  9239  elznn0nn  9243  zltlen  9307  suprzclex  9327  peano2uz2  9336  peano5uzti  9337  qltlen  9616  elfzuzb  9992  4fvwrd4  10113  fzind2  10212  cvg1nlemres  10965  rexfiuz  10969  cbvsum  11339  mertenslem2  11515  mertensabs  11516  cbvprod  11537  prodmodc  11557  fprodseq  11562  ndvdssub  11905  nnwosdc  12010  isprm2  12087  isprm4  12089  hashdvds  12191  isbasis2g  13176  tgval2  13184  elcncf1di  13699  dedekindicclemicc  13743  dedekindicc  13744