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  1937  3exdistr  1967  4exdistr  1968  2sb5  2039  2sb5rf  2045  sbel2x  2054  eu2  2127  euan  2139  sbmo  2142  mo4f  2143  eu4  2145  moanim  2157  2eu4  2176  clelab  2362  nonconne  2426  r2exf  2562  ceqsex3v  2859  ceqsex4v  2860  ceqsex8v  2862  reu2  3008  reu6  3009  reu4  3014  reu7  3015  rmo3f  3017  rmo4f  3018  2rmorex  3026  rmo3  3138  raldifb  3363  inass  3435  dfss4st  3458  ssddif  3459  difin  3462  invdif  3467  indif  3468  indi  3472  difundi  3477  difindiss  3479  inssdif0im  3580  rexdifpr  3722  ssdifsn  3826  unipr  3933  uniun  3938  uniin  3939  iunin2  4060  iindif2m  4064  iinin2m  4065  elpwpw  4083  unidif0  4285  mss  4347  eqvinop  4364  opcom  4372  opeqsn  4374  uniuni  4577  zfinf2  4716  elomssom  4732  fconstmpt  4802  opeliunxp  4810  xpundi  4811  elvvv  4818  xpiindim  4897  elcnv2  4938  cnvuni  4946  dmuni  4971  opelres  5048  restidsing  5099  elima3  5113  imai  5123  imainss  5183  ssrnres  5210  cnvresima  5257  mptpreima  5261  coundir  5270  rnco  5274  coass  5286  relrelss  5294  dffun2  5367  dffun4  5368  dffun6f  5370  dffun4f  5373  dffun7  5384  dffun8  5385  dffun9  5386  svrelfun  5426  fncnv  5427  funcnvuni  5430  dfmpt3  5486  fintm  5557  fin  5558  dff12  5577  fores  5605  dff1o4  5627  eqfnfv3  5782  unpreima  5807  ffnfvf  5841  dff13f  5949  ffnov  6165  eqfnov  6168  foov  6209  opabex3d  6323  opabex3  6324  uchoice  6344  mpoxopovel  6485  tpostpos  6508  dfsmo2  6531  tfr1onlemaccex  6592  tfrcllembxssdm  6600  tfrcllemaccex  6605  tfrcllemres  6606  tfrcldm  6607  erinxp  6856  mapsncnv  6943  cbvixp  6963  ixpin  6971  ixpiinm  6972  mptelixpg  6982  elixpsn  6983  ixpsnf1o  6984  mapsnen  7066  xpassen  7094  2omap  7282  2omotaplemap  7587  distrnqg  7718  subhalfnqq  7745  enq0enq  7762  enq0sym  7763  enq0tr  7765  addnq0mo  7778  mulnq0mo  7779  distrnq0  7790  prarloc  7834  nqprrnd  7874  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemdisj  7937  ltexprlemloc  7938  recexprlemdisj  7961  caucvgprprlemell  8016  caucvgprprlemelu  8017  addsrmo  8074  mulsrmo  8075  opelreal  8158  axcaucvglemres  8230  axpre-suploc  8233  elnnz  9604  elznn0nn  9608  zltlen  9674  suprzclex  9694  peano2uz2  9703  peano5uzti  9704  qltlen  9990  elfzuzb  10372  4fvwrd4  10496  fzind2  10607  cvg1nlemres  11695  rexfiuz  11699  cbvsum  12070  mertenslem2  12247  mertensabs  12248  cbvprod  12269  prodmodc  12289  fprodseq  12294  ndvdssub  12641  bitsmod  12667  nnwosdc  12760  isprm2  12839  isprm4  12841  hashdvds  12943  xpscf  13611  fngsum  13651  igsumvalx  13652  isnsg2  13956  isnsg4  13965  isrhm  14403  issubrng  14445  subsubrng2  14461  subsubrg2  14492  isbasis2g  15036  tgval2  15042  elcncf1di  15570  dedekindicclemicc  15623  dedekindicc  15624  plyco  15750  isclwwlk  16515  clwwlknon2x  16556  iseupthf1o  16569