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  842  19.27h  1582  19.27  1583  19.41  1708  sbcof2  1832  sbidm  1873  sb6  1909  3exdistr  1938  4exdistr  1939  2sb5  2010  2sb5rf  2016  sbel2x  2025  eu2  2097  euan  2109  sbmo  2112  mo4f  2113  eu4  2115  moanim  2127  2eu4  2146  clelab  2330  nonconne  2387  r2exf  2523  ceqsex3v  2814  ceqsex4v  2815  ceqsex8v  2817  reu2  2960  reu6  2961  reu4  2966  reu7  2967  rmo3f  2969  rmo4f  2970  2rmorex  2978  rmo3  3089  raldifb  3312  inass  3382  dfss4st  3405  ssddif  3406  difin  3409  invdif  3414  indif  3415  indi  3419  difundi  3424  difindiss  3426  inssdif0im  3527  rexdifpr  3660  ssdifsn  3760  unipr  3863  uniun  3868  uniin  3869  iunin2  3990  iindif2m  3994  iinin2m  3995  elpwpw  4013  unidif0  4210  mss  4269  eqvinop  4286  opcom  4294  opeqsn  4296  uniuni  4497  zfinf2  4636  elomssom  4652  fconstmpt  4721  opeliunxp  4729  xpundi  4730  elvvv  4737  xpiindim  4814  elcnv2  4855  cnvuni  4863  dmuni  4887  opelres  4963  restidsing  5014  elima3  5028  imai  5037  imainss  5097  ssrnres  5124  cnvresima  5171  mptpreima  5175  coundir  5184  rnco  5188  coass  5200  relrelss  5208  dffun2  5280  dffun4  5281  dffun6f  5283  dffun4f  5286  dffun7  5297  dffun8  5298  dffun9  5299  svrelfun  5338  fncnv  5339  funcnvuni  5342  dfmpt3  5397  fintm  5460  fin  5461  dff12  5479  fores  5507  dff1o4  5529  eqfnfv3  5678  unpreima  5704  ffnfvf  5738  dff13f  5838  ffnov  6048  eqfnov  6051  foov  6092  opabex3d  6205  opabex3  6206  uchoice  6222  mpoxopovel  6326  tpostpos  6349  dfsmo2  6372  tfr1onlemaccex  6433  tfrcllembxssdm  6441  tfrcllemaccex  6446  tfrcllemres  6447  tfrcldm  6448  erinxp  6695  mapsncnv  6781  cbvixp  6801  ixpin  6809  ixpiinm  6810  mptelixpg  6820  elixpsn  6821  ixpsnf1o  6822  mapsnen  6902  xpassen  6924  2omotaplemap  7368  distrnqg  7499  subhalfnqq  7526  enq0enq  7543  enq0sym  7544  enq0tr  7546  addnq0mo  7559  mulnq0mo  7560  distrnq0  7571  prarloc  7615  nqprrnd  7655  ltexprlemopl  7713  ltexprlemlol  7714  ltexprlemopu  7715  ltexprlemupu  7716  ltexprlemdisj  7718  ltexprlemloc  7719  recexprlemdisj  7742  caucvgprprlemell  7797  caucvgprprlemelu  7798  addsrmo  7855  mulsrmo  7856  opelreal  7939  axcaucvglemres  8011  axpre-suploc  8014  elnnz  9381  elznn0nn  9385  zltlen  9450  suprzclex  9470  peano2uz2  9479  peano5uzti  9480  qltlen  9760  elfzuzb  10140  4fvwrd4  10261  fzind2  10366  cvg1nlemres  11238  rexfiuz  11242  cbvsum  11613  mertenslem2  11789  mertensabs  11790  cbvprod  11811  prodmodc  11831  fprodseq  11836  ndvdssub  12183  bitsmod  12209  nnwosdc  12302  isprm2  12381  isprm4  12383  hashdvds  12485  xpscf  13121  fngsum  13162  igsumvalx  13163  isnsg2  13481  isnsg4  13490  isrhm  13862  issubrng  13903  subsubrng2  13919  subsubrg2  13950  isbasis2g  14459  tgval2  14465  elcncf1di  14993  dedekindicclemicc  15046  dedekindicc  15047  plyco  15173  2omap  15865