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	|- ( ph <-> ps )

Assertion

Ref	Expression
anbi2i	|- ( ( ch /\ ph ) <-> ( ch /\ ps ) )

Proof of Theorem anbi2i

Step	Hyp	Ref	Expression
1		bi.aa	. . 3 |- ( ph <-> ps )
2	1	a1i 9	. 2 |- ( ch -> ( ph <-> ps ) )
3	2	pm5.32i 454	1 |- ( ( ch /\ ph ) <-> ( ch /\ ps ) )

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  7340  distrnqg  7471  subhalfnqq  7498  enq0enq  7515  enq0sym  7516  enq0tr  7518  addnq0mo  7531  mulnq0mo  7532  distrnq0  7543  prarloc  7587  nqprrnd  7627  ltexprlemopl  7685  ltexprlemlol  7686  ltexprlemopu  7687  ltexprlemupu  7688  ltexprlemdisj  7690  ltexprlemloc  7691  recexprlemdisj  7714  caucvgprprlemell  7769  caucvgprprlemelu  7770  addsrmo  7827  mulsrmo  7828  opelreal  7911  axcaucvglemres  7983  axpre-suploc  7986  elnnz  9353  elznn0nn  9357  zltlen  9421  suprzclex  9441  peano2uz2  9450  peano5uzti  9451  qltlen  9731  elfzuzb  10111  4fvwrd4  10232  fzind2  10332  cvg1nlemres  11167  rexfiuz  11171  cbvsum  11542  mertenslem2  11718  mertensabs  11719  cbvprod  11740  prodmodc  11760  fprodseq  11765  ndvdssub  12112  bitsmod  12138  nnwosdc  12231  isprm2  12310  isprm4  12312  hashdvds  12414  xpscf  13049  fngsum  13090  igsumvalx  13091  isnsg2  13409  isnsg4  13418  isrhm  13790  issubrng  13831  subsubrng2  13847  subsubrg2  13878  isbasis2g  14365  tgval2  14371  elcncf1di  14899  dedekindicclemicc  14952  dedekindicc  14953  plyco  15079  2omap  15726