Theorem anbi2i 454

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 451	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  457  bianass  466  mpan10  471  an4  581  an42  582  anandir  586  dcim  836  19.27h  1553  19.27  1554  19.41  1679  sbcof2  1803  sbidm  1844  sb6  1879  3exdistr  1908  4exdistr  1909  2sb5  1976  2sb5rf  1982  sbel2x  1991  eu2  2063  euan  2075  sbmo  2078  mo4f  2079  eu4  2081  moanim  2093  2eu4  2112  clelab  2296  nonconne  2352  r2exf  2488  ceqsex3v  2772  ceqsex4v  2773  ceqsex8v  2775  reu2  2918  reu6  2919  reu4  2924  reu7  2925  rmo3f  2927  rmo4f  2928  2rmorex  2936  rmo3  3046  raldifb  3267  inass  3337  dfss4st  3360  ssddif  3361  difin  3364  invdif  3369  indif  3370  indi  3374  difundi  3379  difindiss  3381  inssdif0im  3482  rexdifpr  3611  ssdifsn  3711  unipr  3810  uniun  3815  uniin  3816  iunin2  3936  iindif2m  3940  iinin2m  3941  elpwpw  3959  unidif0  4153  mss  4211  eqvinop  4228  opcom  4235  opeqsn  4237  uniuni  4436  zfinf2  4573  elomssom  4589  fconstmpt  4658  opeliunxp  4666  xpundi  4667  elvvv  4674  xpiindim  4748  elcnv2  4789  cnvuni  4797  dmuni  4821  opelres  4896  elima3  4960  imai  4967  imainss  5026  ssrnres  5053  cnvresima  5100  mptpreima  5104  coundir  5113  rnco  5117  coass  5129  relrelss  5137  dffun2  5208  dffun4  5209  dffun6f  5211  dffun4f  5214  dffun7  5225  dffun8  5226  dffun9  5227  svrelfun  5263  fncnv  5264  funcnvuni  5267  dfmpt3  5320  fintm  5383  fin  5384  dff12  5402  fores  5429  dff1o4  5450  eqfnfv3  5595  unpreima  5621  ffnfvf  5655  dff13f  5749  ffnov  5957  eqfnov  5959  foov  5999  opabex3d  6100  opabex3  6101  mpoxopovel  6220  tpostpos  6243  dfsmo2  6266  tfr1onlemaccex  6327  tfrcllembxssdm  6335  tfrcllemaccex  6340  tfrcllemres  6341  tfrcldm  6342  erinxp  6587  mapsncnv  6673  cbvixp  6693  ixpin  6701  ixpiinm  6702  mptelixpg  6712  elixpsn  6713  ixpsnf1o  6714  mapsnen  6789  xpassen  6808  distrnqg  7349  subhalfnqq  7376  enq0enq  7393  enq0sym  7394  enq0tr  7396  addnq0mo  7409  mulnq0mo  7410  distrnq0  7421  prarloc  7465  nqprrnd  7505  ltexprlemopl  7563  ltexprlemlol  7564  ltexprlemopu  7565  ltexprlemupu  7566  ltexprlemdisj  7568  ltexprlemloc  7569  recexprlemdisj  7592  caucvgprprlemell  7647  caucvgprprlemelu  7648  addsrmo  7705  mulsrmo  7706  opelreal  7789  axcaucvglemres  7861  axpre-suploc  7864  elnnz  9222  elznn0nn  9226  zltlen  9290  suprzclex  9310  peano2uz2  9319  peano5uzti  9320  qltlen  9599  elfzuzb  9975  4fvwrd4  10096  fzind2  10195  cvg1nlemres  10949  rexfiuz  10953  cbvsum  11323  mertenslem2  11499  mertensabs  11500  cbvprod  11521  prodmodc  11541  fprodseq  11546  ndvdssub  11889  nnwosdc  11994  isprm2  12071  isprm4  12073  hashdvds  12175  isbasis2g  12837  tgval2  12845  elcncf1di  13360  dedekindicclemicc  13404  dedekindicc  13405