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  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  2779  ceqsex4v  2780  ceqsex8v  2782  reu2  2925  reu6  2926  reu4  2931  reu7  2932  rmo3f  2934  rmo4f  2935  2rmorex  2943  rmo3  3054  raldifb  3275  inass  3345  dfss4st  3368  ssddif  3369  difin  3372  invdif  3377  indif  3378  indi  3382  difundi  3387  difindiss  3389  inssdif0im  3490  rexdifpr  3620  ssdifsn  3720  unipr  3822  uniun  3827  uniin  3828  iunin2  3948  iindif2m  3952  iinin2m  3953  elpwpw  3971  unidif0  4165  mss  4224  eqvinop  4241  opcom  4248  opeqsn  4250  uniuni  4449  zfinf2  4586  elomssom  4602  fconstmpt  4671  opeliunxp  4679  xpundi  4680  elvvv  4687  xpiindim  4761  elcnv2  4802  cnvuni  4810  dmuni  4834  opelres  4909  restidsing  4960  elima3  4974  imai  4981  imainss  5041  ssrnres  5068  cnvresima  5115  mptpreima  5119  coundir  5128  rnco  5132  coass  5144  relrelss  5152  dffun2  5223  dffun4  5224  dffun6f  5226  dffun4f  5229  dffun7  5240  dffun8  5241  dffun9  5242  svrelfun  5278  fncnv  5279  funcnvuni  5282  dfmpt3  5335  fintm  5398  fin  5399  dff12  5417  fores  5444  dff1o4  5466  eqfnfv3  5612  unpreima  5638  ffnfvf  5672  dff13f  5766  ffnov  5974  eqfnov  5976  foov  6016  opabex3d  6117  opabex3  6118  mpoxopovel  6237  tpostpos  6260  dfsmo2  6283  tfr1onlemaccex  6344  tfrcllembxssdm  6352  tfrcllemaccex  6357  tfrcllemres  6358  tfrcldm  6359  erinxp  6604  mapsncnv  6690  cbvixp  6710  ixpin  6718  ixpiinm  6719  mptelixpg  6729  elixpsn  6730  ixpsnf1o  6731  mapsnen  6806  xpassen  6825  2omotaplemap  7251  distrnqg  7381  subhalfnqq  7408  enq0enq  7425  enq0sym  7426  enq0tr  7428  addnq0mo  7441  mulnq0mo  7442  distrnq0  7453  prarloc  7497  nqprrnd  7537  ltexprlemopl  7595  ltexprlemlol  7596  ltexprlemopu  7597  ltexprlemupu  7598  ltexprlemdisj  7600  ltexprlemloc  7601  recexprlemdisj  7624  caucvgprprlemell  7679  caucvgprprlemelu  7680  addsrmo  7737  mulsrmo  7738  opelreal  7821  axcaucvglemres  7893  axpre-suploc  7896  elnnz  9257  elznn0nn  9261  zltlen  9325  suprzclex  9345  peano2uz2  9354  peano5uzti  9355  qltlen  9634  elfzuzb  10012  4fvwrd4  10133  fzind2  10232  cvg1nlemres  10985  rexfiuz  10989  cbvsum  11359  mertenslem2  11535  mertensabs  11536  cbvprod  11557  prodmodc  11577  fprodseq  11582  ndvdssub  11925  nnwosdc  12030  isprm2  12107  isprm4  12109  hashdvds  12211  isbasis2g  13325  tgval2  13333  elcncf1di  13848  dedekindicclemicc  13892  dedekindicc  13893