Theorem anbi2i 452

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 449	1 ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi12i  455  mpan10  465  an4  575  an42  576  anandir  580  dcim  826  19.27h  1539  19.27  1540  19.41  1664  sbcof2  1782  sbidm  1823  sb6  1858  3exdistr  1887  4exdistr  1888  2sb5  1958  2sb5rf  1964  sbel2x  1973  eu2  2043  euan  2055  sbmo  2058  mo4f  2059  eu4  2061  moanim  2073  2eu4  2092  clelab  2265  nonconne  2320  r2exf  2453  ceqsex3v  2728  ceqsex4v  2729  ceqsex8v  2731  reu2  2872  reu6  2873  reu4  2878  reu7  2879  rmo3f  2881  rmo4f  2882  2rmorex  2890  rmo3  3000  raldifb  3216  inass  3286  dfss4st  3309  ssddif  3310  difin  3313  invdif  3318  indif  3319  indi  3323  difundi  3328  difindiss  3330  inssdif0im  3430  ssdifsn  3651  unipr  3750  uniun  3755  uniin  3756  iunin2  3876  iindif2m  3880  iinin2m  3881  elpwpw  3899  unidif0  4091  mss  4148  eqvinop  4165  opcom  4172  opeqsn  4174  uniuni  4372  zfinf2  4503  elnn  4519  fconstmpt  4586  opeliunxp  4594  xpundi  4595  elvvv  4602  xpiindim  4676  elcnv2  4717  cnvuni  4725  dmuni  4749  opelres  4824  elima3  4888  imai  4895  imainss  4954  ssrnres  4981  cnvresima  5028  mptpreima  5032  coundir  5041  rnco  5045  coass  5057  relrelss  5065  dffun2  5133  dffun4  5134  dffun6f  5136  dffun4f  5139  dffun7  5150  dffun8  5151  dffun9  5152  svrelfun  5188  fncnv  5189  funcnvuni  5192  dfmpt3  5245  fintm  5308  fin  5309  dff12  5327  fores  5354  dff1o4  5375  eqfnfv3  5520  unpreima  5545  ffnfvf  5579  dff13f  5671  ffnov  5875  eqfnov  5877  foov  5917  opabex3d  6019  opabex3  6020  mpoxopovel  6138  tpostpos  6161  dfsmo2  6184  tfr1onlemaccex  6245  tfrcllembxssdm  6253  tfrcllemaccex  6258  tfrcllemres  6259  tfrcldm  6260  erinxp  6503  mapsncnv  6589  cbvixp  6609  ixpin  6617  ixpiinm  6618  mptelixpg  6628  elixpsn  6629  ixpsnf1o  6630  mapsnen  6705  xpassen  6724  distrnqg  7195  subhalfnqq  7222  enq0enq  7239  enq0sym  7240  enq0tr  7242  addnq0mo  7255  mulnq0mo  7256  distrnq0  7267  prarloc  7311  nqprrnd  7351  ltexprlemopl  7409  ltexprlemlol  7410  ltexprlemopu  7411  ltexprlemupu  7412  ltexprlemdisj  7414  ltexprlemloc  7415  recexprlemdisj  7438  caucvgprprlemell  7493  caucvgprprlemelu  7494  addsrmo  7551  mulsrmo  7552  opelreal  7635  axcaucvglemres  7707  axpre-suploc  7710  elnnz  9064  elznn0nn  9068  zltlen  9129  suprzclex  9149  peano2uz2  9158  peano5uzti  9159  qltlen  9432  elfzuzb  9800  4fvwrd4  9917  fzind2  10016  cvg1nlemres  10757  rexfiuz  10761  cbvsum  11129  mertenslem2  11305  mertensabs  11306  cbvprod  11327  prodmodc  11347  ndvdssub  11627  isprm2  11798  isprm4  11800  hashdvds  11897  isbasis2g  12212  tgval2  12220  elcncf1di  12735  dedekindicclemicc  12779  dedekindicc  12780