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  2803  ceqsex4v  2804  ceqsex8v  2806  reu2  2949  reu6  2950  reu4  2955  reu7  2956  rmo3f  2958  rmo4f  2959  2rmorex  2967  rmo3  3078  raldifb  3300  inass  3370  dfss4st  3393  ssddif  3394  difin  3397  invdif  3402  indif  3403  indi  3407  difundi  3412  difindiss  3414  inssdif0im  3515  rexdifpr  3647  ssdifsn  3747  unipr  3850  uniun  3855  uniin  3856  iunin2  3977  iindif2m  3981  iinin2m  3982  elpwpw  4000  unidif0  4197  mss  4256  eqvinop  4273  opcom  4280  opeqsn  4282  uniuni  4483  zfinf2  4622  elomssom  4638  fconstmpt  4707  opeliunxp  4715  xpundi  4716  elvvv  4723  xpiindim  4800  elcnv2  4841  cnvuni  4849  dmuni  4873  opelres  4948  restidsing  4999  elima3  5013  imai  5022  imainss  5082  ssrnres  5109  cnvresima  5156  mptpreima  5160  coundir  5169  rnco  5173  coass  5185  relrelss  5193  dffun2  5265  dffun4  5266  dffun6f  5268  dffun4f  5271  dffun7  5282  dffun8  5283  dffun9  5284  svrelfun  5320  fncnv  5321  funcnvuni  5324  dfmpt3  5377  fintm  5440  fin  5441  dff12  5459  fores  5487  dff1o4  5509  eqfnfv3  5658  unpreima  5684  ffnfvf  5718  dff13f  5814  ffnov  6023  eqfnov  6026  foov  6067  opabex3d  6175  opabex3  6176  uchoice  6192  mpoxopovel  6296  tpostpos  6319  dfsmo2  6342  tfr1onlemaccex  6403  tfrcllembxssdm  6411  tfrcllemaccex  6416  tfrcllemres  6417  tfrcldm  6418  erinxp  6665  mapsncnv  6751  cbvixp  6771  ixpin  6779  ixpiinm  6780  mptelixpg  6790  elixpsn  6791  ixpsnf1o  6792  mapsnen  6867  xpassen  6886  2omotaplemap  7319  distrnqg  7449  subhalfnqq  7476  enq0enq  7493  enq0sym  7494  enq0tr  7496  addnq0mo  7509  mulnq0mo  7510  distrnq0  7521  prarloc  7565  nqprrnd  7605  ltexprlemopl  7663  ltexprlemlol  7664  ltexprlemopu  7665  ltexprlemupu  7666  ltexprlemdisj  7668  ltexprlemloc  7669  recexprlemdisj  7692  caucvgprprlemell  7747  caucvgprprlemelu  7748  addsrmo  7805  mulsrmo  7806  opelreal  7889  axcaucvglemres  7961  axpre-suploc  7964  elnnz  9330  elznn0nn  9334  zltlen  9398  suprzclex  9418  peano2uz2  9427  peano5uzti  9428  qltlen  9708  elfzuzb  10088  4fvwrd4  10209  fzind2  10309  cvg1nlemres  11132  rexfiuz  11136  cbvsum  11506  mertenslem2  11682  mertensabs  11683  cbvprod  11704  prodmodc  11724  fprodseq  11729  ndvdssub  12074  nnwosdc  12179  isprm2  12258  isprm4  12260  hashdvds  12362  xpscf  12933  fngsum  12974  igsumvalx  12975  isnsg2  13276  isnsg4  13285  isrhm  13657  issubrng  13698  subsubrng2  13714  subsubrg2  13745  isbasis2g  14224  tgval2  14230  elcncf1di  14758  dedekindicclemicc  14811  dedekindicc  14812  plyco  14937