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  588  an42  589  anandir  595  dcim  848  19.27h  1608  19.27  1609  19.41  1733  sbcof2  1857  sbidm  1898  sb6  1934  3exdistr  1963  4exdistr  1964  2sb5  2035  2sb5rf  2041  sbel2x  2050  eu2  2123  euan  2135  sbmo  2138  mo4f  2139  eu4  2141  moanim  2153  2eu4  2172  clelab  2356  nonconne  2413  r2exf  2549  ceqsex3v  2845  ceqsex4v  2846  ceqsex8v  2848  reu2  2993  reu6  2994  reu4  2999  reu7  3000  rmo3f  3002  rmo4f  3003  2rmorex  3011  rmo3  3123  raldifb  3346  inass  3416  dfss4st  3439  ssddif  3440  difin  3443  invdif  3448  indif  3449  indi  3453  difundi  3458  difindiss  3460  inssdif0im  3561  rexdifpr  3696  ssdifsn  3800  unipr  3906  uniun  3911  uniin  3912  iunin2  4033  iindif2m  4037  iinin2m  4038  elpwpw  4056  unidif0  4256  mss  4317  eqvinop  4334  opcom  4342  opeqsn  4344  uniuni  4547  zfinf2  4686  elomssom  4702  fconstmpt  4772  opeliunxp  4780  xpundi  4781  elvvv  4788  xpiindim  4866  elcnv2  4907  cnvuni  4915  dmuni  4940  opelres  5017  restidsing  5068  elima3  5082  imai  5091  imainss  5151  ssrnres  5178  cnvresima  5225  mptpreima  5229  coundir  5238  rnco  5242  coass  5254  relrelss  5262  dffun2  5335  dffun4  5336  dffun6f  5338  dffun4f  5341  dffun7  5352  dffun8  5353  dffun9  5354  svrelfun  5394  fncnv  5395  funcnvuni  5398  dfmpt3  5454  fintm  5521  fin  5522  dff12  5541  fores  5569  dff1o4  5591  eqfnfv3  5746  unpreima  5772  ffnfvf  5806  dff13f  5913  ffnov  6127  eqfnov  6130  foov  6171  opabex3d  6285  opabex3  6286  uchoice  6302  mpoxopovel  6409  tpostpos  6432  dfsmo2  6455  tfr1onlemaccex  6516  tfrcllembxssdm  6524  tfrcllemaccex  6529  tfrcllemres  6530  tfrcldm  6531  erinxp  6780  mapsncnv  6866  cbvixp  6886  ixpin  6894  ixpiinm  6895  mptelixpg  6905  elixpsn  6906  ixpsnf1o  6907  mapsnen  6988  xpassen  7016  2omotaplemap  7478  distrnqg  7609  subhalfnqq  7636  enq0enq  7653  enq0sym  7654  enq0tr  7656  addnq0mo  7669  mulnq0mo  7670  distrnq0  7681  prarloc  7725  nqprrnd  7765  ltexprlemopl  7823  ltexprlemlol  7824  ltexprlemopu  7825  ltexprlemupu  7826  ltexprlemdisj  7828  ltexprlemloc  7829  recexprlemdisj  7852  caucvgprprlemell  7907  caucvgprprlemelu  7908  addsrmo  7965  mulsrmo  7966  opelreal  8049  axcaucvglemres  8121  axpre-suploc  8124  elnnz  9491  elznn0nn  9495  zltlen  9560  suprzclex  9580  peano2uz2  9589  peano5uzti  9590  qltlen  9876  elfzuzb  10256  4fvwrd4  10377  fzind2  10488  cvg1nlemres  11565  rexfiuz  11569  cbvsum  11940  mertenslem2  12117  mertensabs  12118  cbvprod  12139  prodmodc  12159  fprodseq  12164  ndvdssub  12511  bitsmod  12537  nnwosdc  12630  isprm2  12709  isprm4  12711  hashdvds  12813  xpscf  13450  fngsum  13491  igsumvalx  13492  isnsg2  13810  isnsg4  13819  isrhm  14193  issubrng  14234  subsubrng2  14250  subsubrg2  14281  isbasis2g  14795  tgval2  14801  elcncf1di  15329  dedekindicclemicc  15382  dedekindicc  15383  plyco  15509  isclwwlk  16271  clwwlknon2x  16312  iseupthf1o  16325  2omap  16652