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  593  dcim  846  19.27h  1606  19.27  1607  19.41  1732  sbcof2  1856  sbidm  1897  sb6  1933  3exdistr  1962  4exdistr  1963  2sb5  2034  2sb5rf  2040  sbel2x  2049  eu2  2122  euan  2134  sbmo  2137  mo4f  2138  eu4  2140  moanim  2152  2eu4  2171  clelab  2355  nonconne  2412  r2exf  2548  ceqsex3v  2844  ceqsex4v  2845  ceqsex8v  2847  reu2  2992  reu6  2993  reu4  2998  reu7  2999  rmo3f  3001  rmo4f  3002  2rmorex  3010  rmo3  3122  raldifb  3345  inass  3415  dfss4st  3438  ssddif  3439  difin  3442  invdif  3447  indif  3448  indi  3452  difundi  3457  difindiss  3459  inssdif0im  3560  rexdifpr  3695  ssdifsn  3799  unipr  3905  uniun  3910  uniin  3911  iunin2  4032  iindif2m  4036  iinin2m  4037  elpwpw  4055  unidif0  4255  mss  4316  eqvinop  4333  opcom  4341  opeqsn  4343  uniuni  4546  zfinf2  4685  elomssom  4701  fconstmpt  4771  opeliunxp  4779  xpundi  4780  elvvv  4787  xpiindim  4865  elcnv2  4906  cnvuni  4914  dmuni  4939  opelres  5016  restidsing  5067  elima3  5081  imai  5090  imainss  5150  ssrnres  5177  cnvresima  5224  mptpreima  5228  coundir  5237  rnco  5241  coass  5253  relrelss  5261  dffun2  5334  dffun4  5335  dffun6f  5337  dffun4f  5340  dffun7  5351  dffun8  5352  dffun9  5353  svrelfun  5392  fncnv  5393  funcnvuni  5396  dfmpt3  5452  fintm  5519  fin  5520  dff12  5538  fores  5566  dff1o4  5588  eqfnfv3  5742  unpreima  5768  ffnfvf  5802  dff13f  5906  ffnov  6120  eqfnov  6123  foov  6164  opabex3d  6278  opabex3  6279  uchoice  6295  mpoxopovel  6402  tpostpos  6425  dfsmo2  6448  tfr1onlemaccex  6509  tfrcllembxssdm  6517  tfrcllemaccex  6522  tfrcllemres  6523  tfrcldm  6524  erinxp  6773  mapsncnv  6859  cbvixp  6879  ixpin  6887  ixpiinm  6888  mptelixpg  6898  elixpsn  6899  ixpsnf1o  6900  mapsnen  6981  xpassen  7009  2omotaplemap  7466  distrnqg  7597  subhalfnqq  7624  enq0enq  7641  enq0sym  7642  enq0tr  7644  addnq0mo  7657  mulnq0mo  7658  distrnq0  7669  prarloc  7713  nqprrnd  7753  ltexprlemopl  7811  ltexprlemlol  7812  ltexprlemopu  7813  ltexprlemupu  7814  ltexprlemdisj  7816  ltexprlemloc  7817  recexprlemdisj  7840  caucvgprprlemell  7895  caucvgprprlemelu  7896  addsrmo  7953  mulsrmo  7954  opelreal  8037  axcaucvglemres  8109  axpre-suploc  8112  elnnz  9479  elznn0nn  9483  zltlen  9548  suprzclex  9568  peano2uz2  9577  peano5uzti  9578  qltlen  9864  elfzuzb  10244  4fvwrd4  10365  fzind2  10475  cvg1nlemres  11536  rexfiuz  11540  cbvsum  11911  mertenslem2  12087  mertensabs  12088  cbvprod  12109  prodmodc  12129  fprodseq  12134  ndvdssub  12481  bitsmod  12507  nnwosdc  12600  isprm2  12679  isprm4  12681  hashdvds  12783  xpscf  13420  fngsum  13461  igsumvalx  13462  isnsg2  13780  isnsg4  13789  isrhm  14162  issubrng  14203  subsubrng2  14219  subsubrg2  14250  isbasis2g  14759  tgval2  14765  elcncf1di  15293  dedekindicclemicc  15346  dedekindicc  15347  plyco  15473  isclwwlk  16189  clwwlknon2x  16230  iseupthf1o  16243  2omap  16530