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  1574  19.27  1575  19.41  1700  sbcof2  1824  sbidm  1865  sb6  1901  3exdistr  1930  4exdistr  1931  2sb5  2002  2sb5rf  2008  sbel2x  2017  eu2  2089  euan  2101  sbmo  2104  mo4f  2105  eu4  2107  moanim  2119  2eu4  2138  clelab  2322  nonconne  2379  r2exf  2515  ceqsex3v  2806  ceqsex4v  2807  ceqsex8v  2809  reu2  2952  reu6  2953  reu4  2958  reu7  2959  rmo3f  2961  rmo4f  2962  2rmorex  2970  rmo3  3081  raldifb  3303  inass  3373  dfss4st  3396  ssddif  3397  difin  3400  invdif  3405  indif  3406  indi  3410  difundi  3415  difindiss  3417  inssdif0im  3518  rexdifpr  3650  ssdifsn  3750  unipr  3853  uniun  3858  uniin  3859  iunin2  3980  iindif2m  3984  iinin2m  3985  elpwpw  4003  unidif0  4200  mss  4259  eqvinop  4276  opcom  4283  opeqsn  4285  uniuni  4486  zfinf2  4625  elomssom  4641  fconstmpt  4710  opeliunxp  4718  xpundi  4719  elvvv  4726  xpiindim  4803  elcnv2  4844  cnvuni  4852  dmuni  4876  opelres  4951  restidsing  5002  elima3  5016  imai  5025  imainss  5085  ssrnres  5112  cnvresima  5159  mptpreima  5163  coundir  5172  rnco  5176  coass  5188  relrelss  5196  dffun2  5268  dffun4  5269  dffun6f  5271  dffun4f  5274  dffun7  5285  dffun8  5286  dffun9  5287  svrelfun  5323  fncnv  5324  funcnvuni  5327  dfmpt3  5380  fintm  5443  fin  5444  dff12  5462  fores  5490  dff1o4  5512  eqfnfv3  5661  unpreima  5687  ffnfvf  5721  dff13f  5817  ffnov  6026  eqfnov  6029  foov  6070  opabex3d  6178  opabex3  6179  uchoice  6195  mpoxopovel  6299  tpostpos  6322  dfsmo2  6345  tfr1onlemaccex  6406  tfrcllembxssdm  6414  tfrcllemaccex  6419  tfrcllemres  6420  tfrcldm  6421  erinxp  6668  mapsncnv  6754  cbvixp  6774  ixpin  6782  ixpiinm  6783  mptelixpg  6793  elixpsn  6794  ixpsnf1o  6795  mapsnen  6870  xpassen  6889  2omotaplemap  7324  distrnqg  7454  subhalfnqq  7481  enq0enq  7498  enq0sym  7499  enq0tr  7501  addnq0mo  7514  mulnq0mo  7515  distrnq0  7526  prarloc  7570  nqprrnd  7610  ltexprlemopl  7668  ltexprlemlol  7669  ltexprlemopu  7670  ltexprlemupu  7671  ltexprlemdisj  7673  ltexprlemloc  7674  recexprlemdisj  7697  caucvgprprlemell  7752  caucvgprprlemelu  7753  addsrmo  7810  mulsrmo  7811  opelreal  7894  axcaucvglemres  7966  axpre-suploc  7969  elnnz  9336  elznn0nn  9340  zltlen  9404  suprzclex  9424  peano2uz2  9433  peano5uzti  9434  qltlen  9714  elfzuzb  10094  4fvwrd4  10215  fzind2  10315  cvg1nlemres  11150  rexfiuz  11154  cbvsum  11525  mertenslem2  11701  mertensabs  11702  cbvprod  11723  prodmodc  11743  fprodseq  11748  ndvdssub  12095  nnwosdc  12206  isprm2  12285  isprm4  12287  hashdvds  12389  xpscf  12990  fngsum  13031  igsumvalx  13032  isnsg2  13333  isnsg4  13342  isrhm  13714  issubrng  13755  subsubrng2  13771  subsubrg2  13802  isbasis2g  14281  tgval2  14287  elcncf1di  14815  dedekindicclemicc  14868  dedekindicc  14869  plyco  14995