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  6182  opabex3  6183  uchoice  6199  mpoxopovel  6303  tpostpos  6326  dfsmo2  6349  tfr1onlemaccex  6410  tfrcllembxssdm  6418  tfrcllemaccex  6423  tfrcllemres  6424  tfrcldm  6425  erinxp  6672  mapsncnv  6758  cbvixp  6778  ixpin  6786  ixpiinm  6787  mptelixpg  6797  elixpsn  6798  ixpsnf1o  6799  mapsnen  6874  xpassen  6893  2omotaplemap  7329  distrnqg  7459  subhalfnqq  7486  enq0enq  7503  enq0sym  7504  enq0tr  7506  addnq0mo  7519  mulnq0mo  7520  distrnq0  7531  prarloc  7575  nqprrnd  7615  ltexprlemopl  7673  ltexprlemlol  7674  ltexprlemopu  7675  ltexprlemupu  7676  ltexprlemdisj  7678  ltexprlemloc  7679  recexprlemdisj  7702  caucvgprprlemell  7757  caucvgprprlemelu  7758  addsrmo  7815  mulsrmo  7816  opelreal  7899  axcaucvglemres  7971  axpre-suploc  7974  elnnz  9341  elznn0nn  9345  zltlen  9409  suprzclex  9429  peano2uz2  9438  peano5uzti  9439  qltlen  9719  elfzuzb  10099  4fvwrd4  10220  fzind2  10320  cvg1nlemres  11155  rexfiuz  11159  cbvsum  11530  mertenslem2  11706  mertensabs  11707  cbvprod  11728  prodmodc  11748  fprodseq  11753  ndvdssub  12100  bitsmod  12126  nnwosdc  12219  isprm2  12298  isprm4  12300  hashdvds  12402  xpscf  13037  fngsum  13078  igsumvalx  13079  isnsg2  13380  isnsg4  13389  isrhm  13761  issubrng  13802  subsubrng2  13818  subsubrg2  13849  isbasis2g  14328  tgval2  14334  elcncf1di  14862  dedekindicclemicc  14915  dedekindicc  14916  plyco  15042  2omap  15689