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  588  an42  589  anandir  595  dcim  849  19.27h  1609  19.27  1610  19.41  1734  sbcof2  1859  sbidm  1900  sb6  1937  3exdistr  1967  4exdistr  1968  2sb5  2039  2sb5rf  2045  sbel2x  2054  eu2  2127  euan  2139  sbmo  2142  mo4f  2143  eu4  2145  moanim  2157  2eu4  2176  clelab  2362  nonconne  2426  r2exf  2562  ceqsex3v  2859  ceqsex4v  2860  ceqsex8v  2862  reu2  3007  reu6  3008  reu4  3013  reu7  3014  rmo3f  3016  rmo4f  3017  2rmorex  3025  rmo3  3137  raldifb  3361  inass  3433  dfss4st  3456  ssddif  3457  difin  3460  invdif  3465  indif  3466  indi  3470  difundi  3475  difindiss  3477  inssdif0im  3578  rexdifpr  3719  ssdifsn  3823  unipr  3930  uniun  3935  uniin  3936  iunin2  4057  iindif2m  4061  iinin2m  4062  elpwpw  4080  unidif0  4282  mss  4344  eqvinop  4361  opcom  4369  opeqsn  4371  uniuni  4574  zfinf2  4713  elomssom  4729  fconstmpt  4799  opeliunxp  4807  xpundi  4808  elvvv  4815  xpiindim  4894  elcnv2  4935  cnvuni  4943  dmuni  4968  opelres  5045  restidsing  5096  elima3  5110  imai  5120  imainss  5180  ssrnres  5207  cnvresima  5254  mptpreima  5258  coundir  5267  rnco  5271  coass  5283  relrelss  5291  dffun2  5364  dffun4  5365  dffun6f  5367  dffun4f  5370  dffun7  5381  dffun8  5382  dffun9  5383  svrelfun  5423  fncnv  5424  funcnvuni  5427  dfmpt3  5483  fintm  5554  fin  5555  dff12  5574  fores  5602  dff1o4  5624  eqfnfv3  5779  unpreima  5804  ffnfvf  5838  dff13f  5945  ffnov  6159  eqfnov  6162  foov  6203  opabex3d  6316  opabex3  6317  uchoice  6333  mpoxopovel  6474  tpostpos  6497  dfsmo2  6520  tfr1onlemaccex  6581  tfrcllembxssdm  6589  tfrcllemaccex  6594  tfrcllemres  6595  tfrcldm  6596  erinxp  6845  mapsncnv  6932  cbvixp  6952  ixpin  6960  ixpiinm  6961  mptelixpg  6971  elixpsn  6972  ixpsnf1o  6973  mapsnen  7055  xpassen  7083  2omap  7271  2omotaplemap  7573  distrnqg  7704  subhalfnqq  7731  enq0enq  7748  enq0sym  7749  enq0tr  7751  addnq0mo  7764  mulnq0mo  7765  distrnq0  7776  prarloc  7820  nqprrnd  7860  ltexprlemopl  7918  ltexprlemlol  7919  ltexprlemopu  7920  ltexprlemupu  7921  ltexprlemdisj  7923  ltexprlemloc  7924  recexprlemdisj  7947  caucvgprprlemell  8002  caucvgprprlemelu  8003  addsrmo  8060  mulsrmo  8061  opelreal  8144  axcaucvglemres  8216  axpre-suploc  8219  elnnz  9589  elznn0nn  9593  zltlen  9659  suprzclex  9679  peano2uz2  9688  peano5uzti  9689  qltlen  9975  elfzuzb  10356  4fvwrd4  10478  fzind2  10589  cvg1nlemres  11674  rexfiuz  11678  cbvsum  12049  mertenslem2  12226  mertensabs  12227  cbvprod  12248  prodmodc  12268  fprodseq  12273  ndvdssub  12620  bitsmod  12646  nnwosdc  12739  isprm2  12818  isprm4  12820  hashdvds  12922  xpscf  13577  fngsum  13618  igsumvalx  13619  isnsg2  13937  isnsg4  13946  isrhm  14320  issubrng  14361  subsubrng2  14377  subsubrg2  14408  isbasis2g  14927  tgval2  14933  elcncf1di  15461  dedekindicclemicc  15514  dedekindicc  15515  plyco  15641  isclwwlk  16406  clwwlknon2x  16447  iseupthf1o  16460