Theorem anbi2i 453

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 450	1 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi12i  456  mpan10  466  an4  576  an42  577  anandir  581  dcim  827  19.27h  1537  19.27  1538  19.41  1663  sbcof2  1787  sbidm  1828  sb6  1863  3exdistr  1892  4exdistr  1893  2sb5  1960  2sb5rf  1966  sbel2x  1975  eu2  2047  euan  2059  sbmo  2062  mo4f  2063  eu4  2065  moanim  2077  2eu4  2096  clelab  2280  nonconne  2336  r2exf  2472  ceqsex3v  2751  ceqsex4v  2752  ceqsex8v  2754  reu2  2896  reu6  2897  reu4  2902  reu7  2903  rmo3f  2905  rmo4f  2906  2rmorex  2914  rmo3  3024  raldifb  3243  inass  3313  dfss4st  3336  ssddif  3337  difin  3340  invdif  3345  indif  3346  indi  3350  difundi  3355  difindiss  3357  inssdif0im  3457  rexdifpr  3584  ssdifsn  3683  unipr  3782  uniun  3787  uniin  3788  iunin2  3908  iindif2m  3912  iinin2m  3913  elpwpw  3931  unidif0  4123  mss  4181  eqvinop  4198  opcom  4205  opeqsn  4207  uniuni  4405  zfinf2  4542  elomssom  4558  fconstmpt  4626  opeliunxp  4634  xpundi  4635  elvvv  4642  xpiindim  4716  elcnv2  4757  cnvuni  4765  dmuni  4789  opelres  4864  elima3  4928  imai  4935  imainss  4994  ssrnres  5021  cnvresima  5068  mptpreima  5072  coundir  5081  rnco  5085  coass  5097  relrelss  5105  dffun2  5173  dffun4  5174  dffun6f  5176  dffun4f  5179  dffun7  5190  dffun8  5191  dffun9  5192  svrelfun  5228  fncnv  5229  funcnvuni  5232  dfmpt3  5285  fintm  5348  fin  5349  dff12  5367  fores  5394  dff1o4  5415  eqfnfv3  5560  unpreima  5585  ffnfvf  5619  dff13f  5711  ffnov  5915  eqfnov  5917  foov  5957  opabex3d  6059  opabex3  6060  mpoxopovel  6178  tpostpos  6201  dfsmo2  6224  tfr1onlemaccex  6285  tfrcllembxssdm  6293  tfrcllemaccex  6298  tfrcllemres  6299  tfrcldm  6300  erinxp  6543  mapsncnv  6629  cbvixp  6649  ixpin  6657  ixpiinm  6658  mptelixpg  6668  elixpsn  6669  ixpsnf1o  6670  mapsnen  6745  xpassen  6764  distrnqg  7286  subhalfnqq  7313  enq0enq  7330  enq0sym  7331  enq0tr  7333  addnq0mo  7346  mulnq0mo  7347  distrnq0  7358  prarloc  7402  nqprrnd  7442  ltexprlemopl  7500  ltexprlemlol  7501  ltexprlemopu  7502  ltexprlemupu  7503  ltexprlemdisj  7505  ltexprlemloc  7506  recexprlemdisj  7529  caucvgprprlemell  7584  caucvgprprlemelu  7585  addsrmo  7642  mulsrmo  7643  opelreal  7726  axcaucvglemres  7798  axpre-suploc  7801  elnnz  9156  elznn0nn  9160  zltlen  9221  suprzclex  9241  peano2uz2  9250  peano5uzti  9251  qltlen  9527  elfzuzb  9900  4fvwrd4  10017  fzind2  10116  cvg1nlemres  10862  rexfiuz  10866  cbvsum  11234  mertenslem2  11410  mertensabs  11411  cbvprod  11432  prodmodc  11452  fprodseq  11457  ndvdssub  11794  isprm2  11965  isprm4  11967  hashdvds  12064  isbasis2g  12382  tgval2  12390  elcncf1di  12905  dedekindicclemicc  12949  dedekindicc  12950