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  593  dcim  846  19.27h  1606  19.27  1607  19.41  1732  sbcof2  1856  sbidm  1897  sb6  1933  3exdistr  1962  4exdistr  1963  2sb5  2034  2sb5rf  2040  sbel2x  2049  eu2  2122  euan  2134  sbmo  2137  mo4f  2138  eu4  2140  moanim  2152  2eu4  2171  clelab  2355  nonconne  2412  r2exf  2548  ceqsex3v  2843  ceqsex4v  2844  ceqsex8v  2846  reu2  2991  reu6  2992  reu4  2997  reu7  2998  rmo3f  3000  rmo4f  3001  2rmorex  3009  rmo3  3121  raldifb  3344  inass  3414  dfss4st  3437  ssddif  3438  difin  3441  invdif  3446  indif  3447  indi  3451  difundi  3456  difindiss  3458  inssdif0im  3559  rexdifpr  3694  ssdifsn  3795  unipr  3901  uniun  3906  uniin  3907  iunin2  4028  iindif2m  4032  iinin2m  4033  elpwpw  4051  unidif0  4250  mss  4311  eqvinop  4328  opcom  4336  opeqsn  4338  uniuni  4541  zfinf2  4680  elomssom  4696  fconstmpt  4765  opeliunxp  4773  xpundi  4774  elvvv  4781  xpiindim  4858  elcnv2  4899  cnvuni  4907  dmuni  4932  opelres  5009  restidsing  5060  elima3  5074  imai  5083  imainss  5143  ssrnres  5170  cnvresima  5217  mptpreima  5221  coundir  5230  rnco  5234  coass  5246  relrelss  5254  dffun2  5327  dffun4  5328  dffun6f  5330  dffun4f  5333  dffun7  5344  dffun8  5345  dffun9  5346  svrelfun  5385  fncnv  5386  funcnvuni  5389  dfmpt3  5445  fintm  5510  fin  5511  dff12  5529  fores  5557  dff1o4  5579  eqfnfv3  5733  unpreima  5759  ffnfvf  5793  dff13f  5893  ffnov  6107  eqfnov  6110  foov  6151  opabex3d  6264  opabex3  6265  uchoice  6281  mpoxopovel  6385  tpostpos  6408  dfsmo2  6431  tfr1onlemaccex  6492  tfrcllembxssdm  6500  tfrcllemaccex  6505  tfrcllemres  6506  tfrcldm  6507  erinxp  6754  mapsncnv  6840  cbvixp  6860  ixpin  6868  ixpiinm  6869  mptelixpg  6879  elixpsn  6880  ixpsnf1o  6881  mapsnen  6962  xpassen  6985  2omotaplemap  7439  distrnqg  7570  subhalfnqq  7597  enq0enq  7614  enq0sym  7615  enq0tr  7617  addnq0mo  7630  mulnq0mo  7631  distrnq0  7642  prarloc  7686  nqprrnd  7726  ltexprlemopl  7784  ltexprlemlol  7785  ltexprlemopu  7786  ltexprlemupu  7787  ltexprlemdisj  7789  ltexprlemloc  7790  recexprlemdisj  7813  caucvgprprlemell  7868  caucvgprprlemelu  7869  addsrmo  7926  mulsrmo  7927  opelreal  8010  axcaucvglemres  8082  axpre-suploc  8085  elnnz  9452  elznn0nn  9456  zltlen  9521  suprzclex  9541  peano2uz2  9550  peano5uzti  9551  qltlen  9831  elfzuzb  10211  4fvwrd4  10332  fzind2  10440  cvg1nlemres  11491  rexfiuz  11495  cbvsum  11866  mertenslem2  12042  mertensabs  12043  cbvprod  12064  prodmodc  12084  fprodseq  12089  ndvdssub  12436  bitsmod  12462  nnwosdc  12555  isprm2  12634  isprm4  12636  hashdvds  12738  xpscf  13375  fngsum  13416  igsumvalx  13417  isnsg2  13735  isnsg4  13744  isrhm  14116  issubrng  14157  subsubrng2  14173  subsubrg2  14204  isbasis2g  14713  tgval2  14719  elcncf1di  15247  dedekindicclemicc  15300  dedekindicc  15301  plyco  15427  2omap  16318