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  842  19.27h  1571  19.27  1572  19.41  1697  sbcof2  1821  sbidm  1862  sb6  1898  3exdistr  1927  4exdistr  1928  2sb5  1999  2sb5rf  2005  sbel2x  2014  eu2  2086  euan  2098  sbmo  2101  mo4f  2102  eu4  2104  moanim  2116  2eu4  2135  clelab  2319  nonconne  2376  r2exf  2512  ceqsex3v  2802  ceqsex4v  2803  ceqsex8v  2805  reu2  2948  reu6  2949  reu4  2954  reu7  2955  rmo3f  2957  rmo4f  2958  2rmorex  2966  rmo3  3077  raldifb  3299  inass  3369  dfss4st  3392  ssddif  3393  difin  3396  invdif  3401  indif  3402  indi  3406  difundi  3411  difindiss  3413  inssdif0im  3514  rexdifpr  3646  ssdifsn  3746  unipr  3849  uniun  3854  uniin  3855  iunin2  3976  iindif2m  3980  iinin2m  3981  elpwpw  3999  unidif0  4196  mss  4255  eqvinop  4272  opcom  4279  opeqsn  4281  uniuni  4482  zfinf2  4621  elomssom  4637  fconstmpt  4706  opeliunxp  4714  xpundi  4715  elvvv  4722  xpiindim  4799  elcnv2  4840  cnvuni  4848  dmuni  4872  opelres  4947  restidsing  4998  elima3  5012  imai  5021  imainss  5081  ssrnres  5108  cnvresima  5155  mptpreima  5159  coundir  5168  rnco  5172  coass  5184  relrelss  5192  dffun2  5264  dffun4  5265  dffun6f  5267  dffun4f  5270  dffun7  5281  dffun8  5282  dffun9  5283  svrelfun  5319  fncnv  5320  funcnvuni  5323  dfmpt3  5376  fintm  5439  fin  5440  dff12  5458  fores  5486  dff1o4  5508  eqfnfv3  5657  unpreima  5683  ffnfvf  5717  dff13f  5813  ffnov  6022  eqfnov  6025  foov  6065  opabex3d  6173  opabex3  6174  uchoice  6190  mpoxopovel  6294  tpostpos  6317  dfsmo2  6340  tfr1onlemaccex  6401  tfrcllembxssdm  6409  tfrcllemaccex  6414  tfrcllemres  6415  tfrcldm  6416  erinxp  6663  mapsncnv  6749  cbvixp  6769  ixpin  6777  ixpiinm  6778  mptelixpg  6788  elixpsn  6789  ixpsnf1o  6790  mapsnen  6865  xpassen  6884  2omotaplemap  7317  distrnqg  7447  subhalfnqq  7474  enq0enq  7491  enq0sym  7492  enq0tr  7494  addnq0mo  7507  mulnq0mo  7508  distrnq0  7519  prarloc  7563  nqprrnd  7603  ltexprlemopl  7661  ltexprlemlol  7662  ltexprlemopu  7663  ltexprlemupu  7664  ltexprlemdisj  7666  ltexprlemloc  7667  recexprlemdisj  7690  caucvgprprlemell  7745  caucvgprprlemelu  7746  addsrmo  7803  mulsrmo  7804  opelreal  7887  axcaucvglemres  7959  axpre-suploc  7962  elnnz  9327  elznn0nn  9331  zltlen  9395  suprzclex  9415  peano2uz2  9424  peano5uzti  9425  qltlen  9705  elfzuzb  10085  4fvwrd4  10206  fzind2  10306  cvg1nlemres  11129  rexfiuz  11133  cbvsum  11503  mertenslem2  11679  mertensabs  11680  cbvprod  11701  prodmodc  11721  fprodseq  11726  ndvdssub  12071  nnwosdc  12176  isprm2  12255  isprm4  12257  hashdvds  12359  xpscf  12930  fngsum  12971  igsumvalx  12972  isnsg2  13273  isnsg4  13282  isrhm  13654  issubrng  13695  subsubrng2  13711  subsubrg2  13742  isbasis2g  14213  tgval2  14219  elcncf1di  14734  dedekindicclemicc  14786  dedekindicc  14787