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  841  19.27h  1560  19.27  1561  19.41  1686  sbcof2  1810  sbidm  1851  sb6  1886  3exdistr  1915  4exdistr  1916  2sb5  1983  2sb5rf  1989  sbel2x  1998  eu2  2070  euan  2082  sbmo  2085  mo4f  2086  eu4  2088  moanim  2100  2eu4  2119  clelab  2303  nonconne  2359  r2exf  2495  ceqsex3v  2780  ceqsex4v  2781  ceqsex8v  2783  reu2  2926  reu6  2927  reu4  2932  reu7  2933  rmo3f  2935  rmo4f  2936  2rmorex  2944  rmo3  3055  raldifb  3276  inass  3346  dfss4st  3369  ssddif  3370  difin  3373  invdif  3378  indif  3379  indi  3383  difundi  3388  difindiss  3390  inssdif0im  3491  rexdifpr  3621  ssdifsn  3721  unipr  3824  uniun  3829  uniin  3830  iunin2  3951  iindif2m  3955  iinin2m  3956  elpwpw  3974  unidif0  4168  mss  4227  eqvinop  4244  opcom  4251  opeqsn  4253  uniuni  4452  zfinf2  4589  elomssom  4605  fconstmpt  4674  opeliunxp  4682  xpundi  4683  elvvv  4690  xpiindim  4765  elcnv2  4806  cnvuni  4814  dmuni  4838  opelres  4913  restidsing  4964  elima3  4978  imai  4985  imainss  5045  ssrnres  5072  cnvresima  5119  mptpreima  5123  coundir  5132  rnco  5136  coass  5148  relrelss  5156  dffun2  5227  dffun4  5228  dffun6f  5230  dffun4f  5233  dffun7  5244  dffun8  5245  dffun9  5246  svrelfun  5282  fncnv  5283  funcnvuni  5286  dfmpt3  5339  fintm  5402  fin  5403  dff12  5421  fores  5448  dff1o4  5470  eqfnfv3  5616  unpreima  5642  ffnfvf  5676  dff13f  5771  ffnov  5979  eqfnov  5981  foov  6021  opabex3d  6122  opabex3  6123  mpoxopovel  6242  tpostpos  6265  dfsmo2  6288  tfr1onlemaccex  6349  tfrcllembxssdm  6357  tfrcllemaccex  6362  tfrcllemres  6363  tfrcldm  6364  erinxp  6609  mapsncnv  6695  cbvixp  6715  ixpin  6723  ixpiinm  6724  mptelixpg  6734  elixpsn  6735  ixpsnf1o  6736  mapsnen  6811  xpassen  6830  2omotaplemap  7256  distrnqg  7386  subhalfnqq  7413  enq0enq  7430  enq0sym  7431  enq0tr  7433  addnq0mo  7446  mulnq0mo  7447  distrnq0  7458  prarloc  7502  nqprrnd  7542  ltexprlemopl  7600  ltexprlemlol  7601  ltexprlemopu  7602  ltexprlemupu  7603  ltexprlemdisj  7605  ltexprlemloc  7606  recexprlemdisj  7629  caucvgprprlemell  7684  caucvgprprlemelu  7685  addsrmo  7742  mulsrmo  7743  opelreal  7826  axcaucvglemres  7898  axpre-suploc  7901  elnnz  9263  elznn0nn  9267  zltlen  9331  suprzclex  9351  peano2uz2  9360  peano5uzti  9361  qltlen  9640  elfzuzb  10019  4fvwrd4  10140  fzind2  10239  cvg1nlemres  10994  rexfiuz  10998  cbvsum  11368  mertenslem2  11544  mertensabs  11545  cbvprod  11566  prodmodc  11586  fprodseq  11591  ndvdssub  11935  nnwosdc  12040  isprm2  12117  isprm4  12119  hashdvds  12221  xpscf  12766  isnsg2  13063  isnsg4  13072  subsubrg2  13367  isbasis2g  13548  tgval2  13554  elcncf1di  14069  dedekindicclemicc  14113  dedekindicc  14114