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  843  19.27h  1584  19.27  1585  19.41  1710  sbcof2  1834  sbidm  1875  sb6  1911  3exdistr  1940  4exdistr  1941  2sb5  2012  2sb5rf  2018  sbel2x  2027  eu2  2099  euan  2111  sbmo  2114  mo4f  2115  eu4  2117  moanim  2129  2eu4  2148  clelab  2332  nonconne  2389  r2exf  2525  ceqsex3v  2817  ceqsex4v  2818  ceqsex8v  2820  reu2  2965  reu6  2966  reu4  2971  reu7  2972  rmo3f  2974  rmo4f  2975  2rmorex  2983  rmo3  3094  raldifb  3317  inass  3387  dfss4st  3410  ssddif  3411  difin  3414  invdif  3419  indif  3420  indi  3424  difundi  3429  difindiss  3431  inssdif0im  3532  rexdifpr  3666  ssdifsn  3767  unipr  3870  uniun  3875  uniin  3876  iunin2  3997  iindif2m  4001  iinin2m  4002  elpwpw  4020  unidif0  4219  mss  4278  eqvinop  4295  opcom  4303  opeqsn  4305  uniuni  4506  zfinf2  4645  elomssom  4661  fconstmpt  4730  opeliunxp  4738  xpundi  4739  elvvv  4746  xpiindim  4823  elcnv2  4864  cnvuni  4872  dmuni  4897  opelres  4973  restidsing  5024  elima3  5038  imai  5047  imainss  5107  ssrnres  5134  cnvresima  5181  mptpreima  5185  coundir  5194  rnco  5198  coass  5210  relrelss  5218  dffun2  5290  dffun4  5291  dffun6f  5293  dffun4f  5296  dffun7  5307  dffun8  5308  dffun9  5309  svrelfun  5348  fncnv  5349  funcnvuni  5352  dfmpt3  5408  fintm  5473  fin  5474  dff12  5492  fores  5520  dff1o4  5542  eqfnfv3  5692  unpreima  5718  ffnfvf  5752  dff13f  5852  ffnov  6062  eqfnov  6065  foov  6106  opabex3d  6219  opabex3  6220  uchoice  6236  mpoxopovel  6340  tpostpos  6363  dfsmo2  6386  tfr1onlemaccex  6447  tfrcllembxssdm  6455  tfrcllemaccex  6460  tfrcllemres  6461  tfrcldm  6462  erinxp  6709  mapsncnv  6795  cbvixp  6815  ixpin  6823  ixpiinm  6824  mptelixpg  6834  elixpsn  6835  ixpsnf1o  6836  mapsnen  6917  xpassen  6940  2omotaplemap  7389  distrnqg  7520  subhalfnqq  7547  enq0enq  7564  enq0sym  7565  enq0tr  7567  addnq0mo  7580  mulnq0mo  7581  distrnq0  7592  prarloc  7636  nqprrnd  7676  ltexprlemopl  7734  ltexprlemlol  7735  ltexprlemopu  7736  ltexprlemupu  7737  ltexprlemdisj  7739  ltexprlemloc  7740  recexprlemdisj  7763  caucvgprprlemell  7818  caucvgprprlemelu  7819  addsrmo  7876  mulsrmo  7877  opelreal  7960  axcaucvglemres  8032  axpre-suploc  8035  elnnz  9402  elznn0nn  9406  zltlen  9471  suprzclex  9491  peano2uz2  9500  peano5uzti  9501  qltlen  9781  elfzuzb  10161  4fvwrd4  10282  fzind2  10390  cvg1nlemres  11371  rexfiuz  11375  cbvsum  11746  mertenslem2  11922  mertensabs  11923  cbvprod  11944  prodmodc  11964  fprodseq  11969  ndvdssub  12316  bitsmod  12342  nnwosdc  12435  isprm2  12514  isprm4  12516  hashdvds  12618  xpscf  13254  fngsum  13295  igsumvalx  13296  isnsg2  13614  isnsg4  13623  isrhm  13995  issubrng  14036  subsubrng2  14052  subsubrg2  14083  isbasis2g  14592  tgval2  14598  elcncf1di  15126  dedekindicclemicc  15179  dedekindicc  15180  plyco  15306  2omap  16071