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  1858  sbidm  1899  sb6  1935  3exdistr  1964  4exdistr  1965  2sb5  2036  2sb5rf  2042  sbel2x  2051  eu2  2124  euan  2136  sbmo  2139  mo4f  2140  eu4  2142  moanim  2154  2eu4  2173  clelab  2358  nonconne  2415  r2exf  2551  ceqsex3v  2847  ceqsex4v  2848  ceqsex8v  2850  reu2  2995  reu6  2996  reu4  3001  reu7  3002  rmo3f  3004  rmo4f  3005  2rmorex  3013  rmo3  3125  raldifb  3349  inass  3419  dfss4st  3442  ssddif  3443  difin  3446  invdif  3451  indif  3452  indi  3456  difundi  3461  difindiss  3463  inssdif0im  3564  rexdifpr  3701  ssdifsn  3805  unipr  3912  uniun  3917  uniin  3918  iunin2  4039  iindif2m  4043  iinin2m  4044  elpwpw  4062  unidif0  4263  mss  4324  eqvinop  4341  opcom  4349  opeqsn  4351  uniuni  4554  zfinf2  4693  elomssom  4709  fconstmpt  4779  opeliunxp  4787  xpundi  4788  elvvv  4795  xpiindim  4873  elcnv2  4914  cnvuni  4922  dmuni  4947  opelres  5024  restidsing  5075  elima3  5089  imai  5099  imainss  5159  ssrnres  5186  cnvresima  5233  mptpreima  5237  coundir  5246  rnco  5250  coass  5262  relrelss  5270  dffun2  5343  dffun4  5344  dffun6f  5346  dffun4f  5349  dffun7  5360  dffun8  5361  dffun9  5362  svrelfun  5402  fncnv  5403  funcnvuni  5406  dfmpt3  5462  fintm  5530  fin  5531  dff12  5550  fores  5578  dff1o4  5600  eqfnfv3  5755  unpreima  5780  ffnfvf  5814  dff13f  5921  ffnov  6135  eqfnov  6138  foov  6179  opabex3d  6292  opabex3  6293  uchoice  6309  mpoxopovel  6450  tpostpos  6473  dfsmo2  6496  tfr1onlemaccex  6557  tfrcllembxssdm  6565  tfrcllemaccex  6570  tfrcllemres  6571  tfrcldm  6572  erinxp  6821  mapsncnv  6907  cbvixp  6927  ixpin  6935  ixpiinm  6936  mptelixpg  6946  elixpsn  6947  ixpsnf1o  6948  mapsnen  7029  xpassen  7057  2omotaplemap  7519  distrnqg  7650  subhalfnqq  7677  enq0enq  7694  enq0sym  7695  enq0tr  7697  addnq0mo  7710  mulnq0mo  7711  distrnq0  7722  prarloc  7766  nqprrnd  7806  ltexprlemopl  7864  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemdisj  7869  ltexprlemloc  7870  recexprlemdisj  7893  caucvgprprlemell  7948  caucvgprprlemelu  7949  addsrmo  8006  mulsrmo  8007  opelreal  8090  axcaucvglemres  8162  axpre-suploc  8165  elnnz  9533  elznn0nn  9537  zltlen  9602  suprzclex  9622  peano2uz2  9631  peano5uzti  9632  qltlen  9918  elfzuzb  10299  4fvwrd4  10420  fzind2  10531  cvg1nlemres  11608  rexfiuz  11612  cbvsum  11983  mertenslem2  12160  mertensabs  12161  cbvprod  12182  prodmodc  12202  fprodseq  12207  ndvdssub  12554  bitsmod  12580  nnwosdc  12673  isprm2  12752  isprm4  12754  hashdvds  12856  xpscf  13493  fngsum  13534  igsumvalx  13535  isnsg2  13853  isnsg4  13862  isrhm  14236  issubrng  14277  subsubrng2  14293  subsubrg2  14324  isbasis2g  14839  tgval2  14845  elcncf1di  15373  dedekindicclemicc  15426  dedekindicc  15427  plyco  15553  isclwwlk  16318  clwwlknon2x  16359  iseupthf1o  16372  2omap  16698