Theorem anbi2i 446

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 443	1 |- ( ( ch /\ ph ) <-> ( ch /\ ps ) )

Syntax hints:   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi12i  449  mpan10  459  an4  554  an42  555  anandir  559  dcim  825  19.27h  1504  19.27  1505  19.41  1628  sbcof2  1745  sbidm  1786  sb6  1821  3exdistr  1847  4exdistr  1848  2sb5  1914  2sb5rf  1920  sbel2x  1929  eu2  1999  euan  2011  sbmo  2014  mo4f  2015  eu4  2017  moanim  2029  2eu4  2048  clelab  2219  nonconne  2274  r2exf  2407  ceqsex3v  2675  ceqsex4v  2676  ceqsex8v  2678  reu2  2817  reu6  2818  reu4  2823  reu7  2824  rmo3f  2826  rmo4f  2827  2rmorex  2835  rmo3  2944  raldifb  3155  inass  3225  dfss4st  3248  ssddif  3249  difin  3252  invdif  3257  indif  3258  indi  3262  difundi  3267  difindiss  3269  inssdif0im  3369  ssdifsn  3590  unipr  3689  uniun  3694  uniin  3695  iunin2  3815  iindif2m  3819  iinin2m  3820  elpwpw  3837  unidif0  4023  mss  4077  eqvinop  4094  opcom  4101  opeqsn  4103  uniuni  4301  zfinf2  4432  elnn  4448  fconstmpt  4514  opeliunxp  4522  xpundi  4523  elvvv  4530  xpiindim  4604  elcnv2  4645  cnvuni  4653  dmuni  4677  opelres  4750  elima3  4814  imai  4821  imainss  4880  ssrnres  4907  cnvresima  4954  mptpreima  4958  coundir  4967  rnco  4971  coass  4983  relrelss  4991  dffun2  5059  dffun4  5060  dffun6f  5062  dffun4f  5065  dffun7  5076  dffun8  5077  dffun9  5078  svrelfun  5113  fncnv  5114  funcnvuni  5117  dfmpt3  5170  fintm  5231  fin  5232  dff12  5250  fores  5277  dff1o4  5296  eqfnfv3  5438  unpreima  5463  ffnfvf  5496  dff13f  5587  ffnov  5787  eqfnov  5789  foov  5829  opabex3d  5930  opabex3  5931  mpt2xopovel  6044  tpostpos  6067  dfsmo2  6090  tfr1onlemaccex  6151  tfrcllembxssdm  6159  tfrcllemaccex  6164  tfrcllemres  6165  tfrcldm  6166  erinxp  6406  mapsncnv  6492  cbvixp  6512  ixpin  6520  ixpiinm  6521  mptelixpg  6531  elixpsn  6532  ixpsnf1o  6533  mapsnen  6608  xpassen  6626  distrnqg  7043  subhalfnqq  7070  enq0enq  7087  enq0sym  7088  enq0tr  7090  addnq0mo  7103  mulnq0mo  7104  distrnq0  7115  prarloc  7159  nqprrnd  7199  ltexprlemopl  7257  ltexprlemlol  7258  ltexprlemopu  7259  ltexprlemupu  7260  ltexprlemdisj  7262  ltexprlemloc  7263  recexprlemdisj  7286  caucvgprprlemell  7341  caucvgprprlemelu  7342  addsrmo  7386  mulsrmo  7387  opelreal  7462  axcaucvglemres  7531  elnnz  8858  elznn0nn  8862  zltlen  8923  suprzclex  8943  peano2uz2  8952  peano5uzti  8953  qltlen  9224  elfzuzb  9583  4fvwrd4  9700  fzind2  9799  cvg1nlemres  10533  rexfiuz  10537  cbvsum  10903  mertenslem2  11079  mertensabs  11080  ndvdssub  11357  isprm2  11526  isprm4  11528  hashdvds  11624  isbasis2g  11895  tgval2  11903  elcncf1di  12332