Theorem anbi2i 453

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 450	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  456  mpan10  466  an4  576  an42  577  anandir  581  dcim  827  19.27h  1540  19.27  1541  19.41  1665  sbcof2  1783  sbidm  1824  sb6  1859  3exdistr  1888  4exdistr  1889  2sb5  1959  2sb5rf  1965  sbel2x  1974  eu2  2044  euan  2056  sbmo  2059  mo4f  2060  eu4  2062  moanim  2074  2eu4  2093  clelab  2266  nonconne  2321  r2exf  2456  ceqsex3v  2731  ceqsex4v  2732  ceqsex8v  2734  reu2  2876  reu6  2877  reu4  2882  reu7  2883  rmo3f  2885  rmo4f  2886  2rmorex  2894  rmo3  3004  raldifb  3221  inass  3291  dfss4st  3314  ssddif  3315  difin  3318  invdif  3323  indif  3324  indi  3328  difundi  3333  difindiss  3335  inssdif0im  3435  rexdifpr  3560  ssdifsn  3659  unipr  3758  uniun  3763  uniin  3764  iunin2  3884  iindif2m  3888  iinin2m  3889  elpwpw  3907  unidif0  4099  mss  4156  eqvinop  4173  opcom  4180  opeqsn  4182  uniuni  4380  zfinf2  4511  elnn  4527  fconstmpt  4594  opeliunxp  4602  xpundi  4603  elvvv  4610  xpiindim  4684  elcnv2  4725  cnvuni  4733  dmuni  4757  opelres  4832  elima3  4896  imai  4903  imainss  4962  ssrnres  4989  cnvresima  5036  mptpreima  5040  coundir  5049  rnco  5053  coass  5065  relrelss  5073  dffun2  5141  dffun4  5142  dffun6f  5144  dffun4f  5147  dffun7  5158  dffun8  5159  dffun9  5160  svrelfun  5196  fncnv  5197  funcnvuni  5200  dfmpt3  5253  fintm  5316  fin  5317  dff12  5335  fores  5362  dff1o4  5383  eqfnfv3  5528  unpreima  5553  ffnfvf  5587  dff13f  5679  ffnov  5883  eqfnov  5885  foov  5925  opabex3d  6027  opabex3  6028  mpoxopovel  6146  tpostpos  6169  dfsmo2  6192  tfr1onlemaccex  6253  tfrcllembxssdm  6261  tfrcllemaccex  6266  tfrcllemres  6267  tfrcldm  6268  erinxp  6511  mapsncnv  6597  cbvixp  6617  ixpin  6625  ixpiinm  6626  mptelixpg  6636  elixpsn  6637  ixpsnf1o  6638  mapsnen  6713  xpassen  6732  distrnqg  7219  subhalfnqq  7246  enq0enq  7263  enq0sym  7264  enq0tr  7266  addnq0mo  7279  mulnq0mo  7280  distrnq0  7291  prarloc  7335  nqprrnd  7375  ltexprlemopl  7433  ltexprlemlol  7434  ltexprlemopu  7435  ltexprlemupu  7436  ltexprlemdisj  7438  ltexprlemloc  7439  recexprlemdisj  7462  caucvgprprlemell  7517  caucvgprprlemelu  7518  addsrmo  7575  mulsrmo  7576  opelreal  7659  axcaucvglemres  7731  axpre-suploc  7734  elnnz  9088  elznn0nn  9092  zltlen  9153  suprzclex  9173  peano2uz2  9182  peano5uzti  9183  qltlen  9459  elfzuzb  9831  4fvwrd4  9948  fzind2  10047  cvg1nlemres  10789  rexfiuz  10793  cbvsum  11161  mertenslem2  11337  mertensabs  11338  cbvprod  11359  prodmodc  11379  fprodseq  11384  ndvdssub  11663  isprm2  11834  isprm4  11836  hashdvds  11933  isbasis2g  12251  tgval2  12259  elcncf1di  12774  dedekindicclemicc  12818  dedekindicc  12819