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  2843  ceqsex4v  2844  ceqsex8v  2846  reu2  2991  reu6  2992  reu4  2997  reu7  2998  rmo3f  3000  rmo4f  3001  2rmorex  3009  rmo3  3121  raldifb  3344  inass  3414  dfss4st  3437  ssddif  3438  difin  3441  invdif  3446  indif  3447  indi  3451  difundi  3456  difindiss  3458  inssdif0im  3559  rexdifpr  3694  ssdifsn  3796  unipr  3902  uniun  3907  uniin  3908  iunin2  4029  iindif2m  4033  iinin2m  4034  elpwpw  4052  unidif0  4251  mss  4312  eqvinop  4329  opcom  4337  opeqsn  4339  uniuni  4542  zfinf2  4681  elomssom  4697  fconstmpt  4766  opeliunxp  4774  xpundi  4775  elvvv  4782  xpiindim  4859  elcnv2  4900  cnvuni  4908  dmuni  4933  opelres  5010  restidsing  5061  elima3  5075  imai  5084  imainss  5144  ssrnres  5171  cnvresima  5218  mptpreima  5222  coundir  5231  rnco  5235  coass  5247  relrelss  5255  dffun2  5328  dffun4  5329  dffun6f  5331  dffun4f  5334  dffun7  5345  dffun8  5346  dffun9  5347  svrelfun  5386  fncnv  5387  funcnvuni  5390  dfmpt3  5446  fintm  5513  fin  5514  dff12  5532  fores  5560  dff1o4  5582  eqfnfv3  5736  unpreima  5762  ffnfvf  5796  dff13f  5900  ffnov  6114  eqfnov  6117  foov  6158  opabex3d  6272  opabex3  6273  uchoice  6289  mpoxopovel  6393  tpostpos  6416  dfsmo2  6439  tfr1onlemaccex  6500  tfrcllembxssdm  6508  tfrcllemaccex  6513  tfrcllemres  6514  tfrcldm  6515  erinxp  6764  mapsncnv  6850  cbvixp  6870  ixpin  6878  ixpiinm  6879  mptelixpg  6889  elixpsn  6890  ixpsnf1o  6891  mapsnen  6972  xpassen  6997  2omotaplemap  7454  distrnqg  7585  subhalfnqq  7612  enq0enq  7629  enq0sym  7630  enq0tr  7632  addnq0mo  7645  mulnq0mo  7646  distrnq0  7657  prarloc  7701  nqprrnd  7741  ltexprlemopl  7799  ltexprlemlol  7800  ltexprlemopu  7801  ltexprlemupu  7802  ltexprlemdisj  7804  ltexprlemloc  7805  recexprlemdisj  7828  caucvgprprlemell  7883  caucvgprprlemelu  7884  addsrmo  7941  mulsrmo  7942  opelreal  8025  axcaucvglemres  8097  axpre-suploc  8100  elnnz  9467  elznn0nn  9471  zltlen  9536  suprzclex  9556  peano2uz2  9565  peano5uzti  9566  qltlen  9847  elfzuzb  10227  4fvwrd4  10348  fzind2  10457  cvg1nlemres  11511  rexfiuz  11515  cbvsum  11886  mertenslem2  12062  mertensabs  12063  cbvprod  12084  prodmodc  12104  fprodseq  12109  ndvdssub  12456  bitsmod  12482  nnwosdc  12575  isprm2  12654  isprm4  12656  hashdvds  12758  xpscf  13395  fngsum  13436  igsumvalx  13437  isnsg2  13755  isnsg4  13764  isrhm  14137  issubrng  14178  subsubrng2  14194  subsubrg2  14225  isbasis2g  14734  tgval2  14740  elcncf1di  15268  dedekindicclemicc  15321  dedekindicc  15322  plyco  15448  isclwwlk  16132  2omap  16418