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  843  19.27h  1583  19.27  1584  19.41  1709  sbcof2  1833  sbidm  1874  sb6  1910  3exdistr  1939  4exdistr  1940  2sb5  2011  2sb5rf  2017  sbel2x  2026  eu2  2098  euan  2110  sbmo  2113  mo4f  2114  eu4  2116  moanim  2128  2eu4  2147  clelab  2331  nonconne  2388  r2exf  2524  ceqsex3v  2815  ceqsex4v  2816  ceqsex8v  2818  reu2  2961  reu6  2962  reu4  2967  reu7  2968  rmo3f  2970  rmo4f  2971  2rmorex  2979  rmo3  3090  raldifb  3313  inass  3383  dfss4st  3406  ssddif  3407  difin  3410  invdif  3415  indif  3416  indi  3420  difundi  3425  difindiss  3427  inssdif0im  3528  rexdifpr  3661  ssdifsn  3761  unipr  3864  uniun  3869  uniin  3870  iunin2  3991  iindif2m  3995  iinin2m  3996  elpwpw  4014  unidif0  4211  mss  4270  eqvinop  4287  opcom  4295  opeqsn  4297  uniuni  4498  zfinf2  4637  elomssom  4653  fconstmpt  4722  opeliunxp  4730  xpundi  4731  elvvv  4738  xpiindim  4815  elcnv2  4856  cnvuni  4864  dmuni  4888  opelres  4964  restidsing  5015  elima3  5029  imai  5038  imainss  5098  ssrnres  5125  cnvresima  5172  mptpreima  5176  coundir  5185  rnco  5189  coass  5201  relrelss  5209  dffun2  5281  dffun4  5282  dffun6f  5284  dffun4f  5287  dffun7  5298  dffun8  5299  dffun9  5300  svrelfun  5339  fncnv  5340  funcnvuni  5343  dfmpt3  5398  fintm  5461  fin  5462  dff12  5480  fores  5508  dff1o4  5530  eqfnfv3  5679  unpreima  5705  ffnfvf  5739  dff13f  5839  ffnov  6049  eqfnov  6052  foov  6093  opabex3d  6206  opabex3  6207  uchoice  6223  mpoxopovel  6327  tpostpos  6350  dfsmo2  6373  tfr1onlemaccex  6434  tfrcllembxssdm  6442  tfrcllemaccex  6447  tfrcllemres  6448  tfrcldm  6449  erinxp  6696  mapsncnv  6782  cbvixp  6802  ixpin  6810  ixpiinm  6811  mptelixpg  6821  elixpsn  6822  ixpsnf1o  6823  mapsnen  6903  xpassen  6925  2omotaplemap  7369  distrnqg  7500  subhalfnqq  7527  enq0enq  7544  enq0sym  7545  enq0tr  7547  addnq0mo  7560  mulnq0mo  7561  distrnq0  7572  prarloc  7616  nqprrnd  7656  ltexprlemopl  7714  ltexprlemlol  7715  ltexprlemopu  7716  ltexprlemupu  7717  ltexprlemdisj  7719  ltexprlemloc  7720  recexprlemdisj  7743  caucvgprprlemell  7798  caucvgprprlemelu  7799  addsrmo  7856  mulsrmo  7857  opelreal  7940  axcaucvglemres  8012  axpre-suploc  8015  elnnz  9382  elznn0nn  9386  zltlen  9451  suprzclex  9471  peano2uz2  9480  peano5uzti  9481  qltlen  9761  elfzuzb  10141  4fvwrd4  10262  fzind2  10368  cvg1nlemres  11296  rexfiuz  11300  cbvsum  11671  mertenslem2  11847  mertensabs  11848  cbvprod  11869  prodmodc  11889  fprodseq  11894  ndvdssub  12241  bitsmod  12267  nnwosdc  12360  isprm2  12439  isprm4  12441  hashdvds  12543  xpscf  13179  fngsum  13220  igsumvalx  13221  isnsg2  13539  isnsg4  13548  isrhm  13920  issubrng  13961  subsubrng2  13977  subsubrg2  14008  isbasis2g  14517  tgval2  14523  elcncf1di  15051  dedekindicclemicc  15104  dedekindicc  15105  plyco  15231  2omap  15932