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  849  19.27h  1609  19.27  1610  19.41  1734  sbcof2  1859  sbidm  1900  sb6  1936  3exdistr  1965  4exdistr  1966  2sb5  2037  2sb5rf  2043  sbel2x  2052  eu2  2125  euan  2137  sbmo  2140  mo4f  2141  eu4  2143  moanim  2155  2eu4  2174  clelab  2360  nonconne  2424  r2exf  2560  ceqsex3v  2857  ceqsex4v  2858  ceqsex8v  2860  reu2  3005  reu6  3006  reu4  3011  reu7  3012  rmo3f  3014  rmo4f  3015  2rmorex  3023  rmo3  3135  raldifb  3359  inass  3431  dfss4st  3454  ssddif  3455  difin  3458  invdif  3463  indif  3464  indi  3468  difundi  3473  difindiss  3475  inssdif0im  3576  rexdifpr  3717  ssdifsn  3821  unipr  3928  uniun  3933  uniin  3934  iunin2  4055  iindif2m  4059  iinin2m  4060  elpwpw  4078  unidif0  4280  mss  4342  eqvinop  4359  opcom  4367  opeqsn  4369  uniuni  4572  zfinf2  4711  elomssom  4727  fconstmpt  4797  opeliunxp  4805  xpundi  4806  elvvv  4813  xpiindim  4892  elcnv2  4933  cnvuni  4941  dmuni  4966  opelres  5043  restidsing  5094  elima3  5108  imai  5118  imainss  5178  ssrnres  5205  cnvresima  5252  mptpreima  5256  coundir  5265  rnco  5269  coass  5281  relrelss  5289  dffun2  5362  dffun4  5363  dffun6f  5365  dffun4f  5368  dffun7  5379  dffun8  5380  dffun9  5381  svrelfun  5421  fncnv  5422  funcnvuni  5425  dfmpt3  5481  fintm  5552  fin  5553  dff12  5572  fores  5600  dff1o4  5622  eqfnfv3  5777  unpreima  5802  ffnfvf  5836  dff13f  5943  ffnov  6157  eqfnov  6160  foov  6201  opabex3d  6314  opabex3  6315  uchoice  6331  mpoxopovel  6472  tpostpos  6495  dfsmo2  6518  tfr1onlemaccex  6579  tfrcllembxssdm  6587  tfrcllemaccex  6592  tfrcllemres  6593  tfrcldm  6594  erinxp  6843  mapsncnv  6930  cbvixp  6950  ixpin  6958  ixpiinm  6959  mptelixpg  6969  elixpsn  6970  ixpsnf1o  6971  mapsnen  7053  xpassen  7081  2omap  7269  2omotaplemap  7571  distrnqg  7702  subhalfnqq  7729  enq0enq  7746  enq0sym  7747  enq0tr  7749  addnq0mo  7762  mulnq0mo  7763  distrnq0  7774  prarloc  7818  nqprrnd  7858  ltexprlemopl  7916  ltexprlemlol  7917  ltexprlemopu  7918  ltexprlemupu  7919  ltexprlemdisj  7921  ltexprlemloc  7922  recexprlemdisj  7945  caucvgprprlemell  8000  caucvgprprlemelu  8001  addsrmo  8058  mulsrmo  8059  opelreal  8142  axcaucvglemres  8214  axpre-suploc  8217  elnnz  9587  elznn0nn  9591  zltlen  9656  suprzclex  9676  peano2uz2  9685  peano5uzti  9686  qltlen  9972  elfzuzb  10353  4fvwrd4  10474  fzind2  10585  cvg1nlemres  11670  rexfiuz  11674  cbvsum  12045  mertenslem2  12222  mertensabs  12223  cbvprod  12244  prodmodc  12264  fprodseq  12269  ndvdssub  12616  bitsmod  12642  nnwosdc  12735  isprm2  12814  isprm4  12816  hashdvds  12918  xpscf  13560  fngsum  13601  igsumvalx  13602  isnsg2  13920  isnsg4  13929  isrhm  14303  issubrng  14344  subsubrng2  14360  subsubrg2  14391  isbasis2g  14910  tgval2  14916  elcncf1di  15444  dedekindicclemicc  15497  dedekindicc  15498  plyco  15624  isclwwlk  16389  clwwlknon2x  16430  iseupthf1o  16443