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  3304  inass  3374  dfss4st  3397  ssddif  3398  difin  3401  invdif  3406  indif  3407  indi  3411  difundi  3416  difindiss  3418  inssdif0im  3519  rexdifpr  3651  ssdifsn  3751  unipr  3854  uniun  3859  uniin  3860  iunin2  3981  iindif2m  3985  iinin2m  3986  elpwpw  4004  unidif0  4201  mss  4260  eqvinop  4277  opcom  4284  opeqsn  4286  uniuni  4487  zfinf2  4626  elomssom  4642  fconstmpt  4711  opeliunxp  4719  xpundi  4720  elvvv  4727  xpiindim  4804  elcnv2  4845  cnvuni  4853  dmuni  4877  opelres  4952  restidsing  5003  elima3  5017  imai  5026  imainss  5086  ssrnres  5113  cnvresima  5160  mptpreima  5164  coundir  5173  rnco  5177  coass  5189  relrelss  5197  dffun2  5269  dffun4  5270  dffun6f  5272  dffun4f  5275  dffun7  5286  dffun8  5287  dffun9  5288  svrelfun  5324  fncnv  5325  funcnvuni  5328  dfmpt3  5383  fintm  5446  fin  5447  dff12  5465  fores  5493  dff1o4  5515  eqfnfv3  5664  unpreima  5690  ffnfvf  5724  dff13f  5820  ffnov  6030  eqfnov  6033  foov  6074  opabex3d  6187  opabex3  6188  uchoice  6204  mpoxopovel  6308  tpostpos  6331  dfsmo2  6354  tfr1onlemaccex  6415  tfrcllembxssdm  6423  tfrcllemaccex  6428  tfrcllemres  6429  tfrcldm  6430  erinxp  6677  mapsncnv  6763  cbvixp  6783  ixpin  6791  ixpiinm  6792  mptelixpg  6802  elixpsn  6803  ixpsnf1o  6804  mapsnen  6879  xpassen  6898  2omotaplemap  7342  distrnqg  7473  subhalfnqq  7500  enq0enq  7517  enq0sym  7518  enq0tr  7520  addnq0mo  7533  mulnq0mo  7534  distrnq0  7545  prarloc  7589  nqprrnd  7629  ltexprlemopl  7687  ltexprlemlol  7688  ltexprlemopu  7689  ltexprlemupu  7690  ltexprlemdisj  7692  ltexprlemloc  7693  recexprlemdisj  7716  caucvgprprlemell  7771  caucvgprprlemelu  7772  addsrmo  7829  mulsrmo  7830  opelreal  7913  axcaucvglemres  7985  axpre-suploc  7988  elnnz  9355  elznn0nn  9359  zltlen  9423  suprzclex  9443  peano2uz2  9452  peano5uzti  9453  qltlen  9733  elfzuzb  10113  4fvwrd4  10234  fzind2  10334  cvg1nlemres  11169  rexfiuz  11173  cbvsum  11544  mertenslem2  11720  mertensabs  11721  cbvprod  11742  prodmodc  11762  fprodseq  11767  ndvdssub  12114  bitsmod  12140  nnwosdc  12233  isprm2  12312  isprm4  12314  hashdvds  12416  xpscf  13051  fngsum  13092  igsumvalx  13093  isnsg2  13411  isnsg4  13420  isrhm  13792  issubrng  13833  subsubrng2  13849  subsubrg2  13880  isbasis2g  14389  tgval2  14395  elcncf1di  14923  dedekindicclemicc  14976  dedekindicc  14977  plyco  15103  2omap  15750