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  1858  sbidm  1899  sb6  1935  3exdistr  1964  4exdistr  1965  2sb5  2036  2sb5rf  2042  sbel2x  2051  eu2  2124  euan  2136  sbmo  2139  mo4f  2140  eu4  2142  moanim  2154  2eu4  2173  clelab  2358  nonconne  2415  r2exf  2551  ceqsex3v  2847  ceqsex4v  2848  ceqsex8v  2850  reu2  2995  reu6  2996  reu4  3001  reu7  3002  rmo3f  3004  rmo4f  3005  2rmorex  3013  rmo3  3125  raldifb  3349  inass  3419  dfss4st  3442  ssddif  3443  difin  3446  invdif  3451  indif  3452  indi  3456  difundi  3461  difindiss  3463  inssdif0im  3564  rexdifpr  3701  ssdifsn  3805  unipr  3912  uniun  3917  uniin  3918  iunin2  4039  iindif2m  4043  iinin2m  4044  elpwpw  4062  unidif0  4263  mss  4324  eqvinop  4341  opcom  4349  opeqsn  4351  uniuni  4554  zfinf2  4693  elomssom  4709  fconstmpt  4779  opeliunxp  4787  xpundi  4788  elvvv  4795  xpiindim  4873  elcnv2  4914  cnvuni  4922  dmuni  4947  opelres  5024  restidsing  5075  elima3  5089  imai  5099  imainss  5159  ssrnres  5186  cnvresima  5233  mptpreima  5237  coundir  5246  rnco  5250  coass  5262  relrelss  5270  dffun2  5343  dffun4  5344  dffun6f  5346  dffun4f  5349  dffun7  5360  dffun8  5361  dffun9  5362  svrelfun  5402  fncnv  5403  funcnvuni  5406  dfmpt3  5462  fintm  5530  fin  5531  dff12  5550  fores  5578  dff1o4  5600  eqfnfv3  5755  unpreima  5780  ffnfvf  5814  dff13f  5921  ffnov  6135  eqfnov  6138  foov  6179  opabex3d  6292  opabex3  6293  uchoice  6309  mpoxopovel  6450  tpostpos  6473  dfsmo2  6496  tfr1onlemaccex  6557  tfrcllembxssdm  6565  tfrcllemaccex  6570  tfrcllemres  6571  tfrcldm  6572  erinxp  6821  mapsncnv  6907  cbvixp  6927  ixpin  6935  ixpiinm  6936  mptelixpg  6946  elixpsn  6947  ixpsnf1o  6948  mapsnen  7029  xpassen  7057  2omotaplemap  7536  distrnqg  7667  subhalfnqq  7694  enq0enq  7711  enq0sym  7712  enq0tr  7714  addnq0mo  7727  mulnq0mo  7728  distrnq0  7739  prarloc  7783  nqprrnd  7823  ltexprlemopl  7881  ltexprlemlol  7882  ltexprlemopu  7883  ltexprlemupu  7884  ltexprlemdisj  7886  ltexprlemloc  7887  recexprlemdisj  7910  caucvgprprlemell  7965  caucvgprprlemelu  7966  addsrmo  8023  mulsrmo  8024  opelreal  8107  axcaucvglemres  8179  axpre-suploc  8182  elnnz  9550  elznn0nn  9554  zltlen  9619  suprzclex  9639  peano2uz2  9648  peano5uzti  9649  qltlen  9935  elfzuzb  10316  4fvwrd4  10437  fzind2  10548  cvg1nlemres  11625  rexfiuz  11629  cbvsum  12000  mertenslem2  12177  mertensabs  12178  cbvprod  12199  prodmodc  12219  fprodseq  12224  ndvdssub  12571  bitsmod  12597  nnwosdc  12690  isprm2  12769  isprm4  12771  hashdvds  12873  xpscf  13510  fngsum  13551  igsumvalx  13552  isnsg2  13870  isnsg4  13879  isrhm  14253  issubrng  14294  subsubrng2  14310  subsubrg2  14341  isbasis2g  14856  tgval2  14862  elcncf1di  15390  dedekindicclemicc  15443  dedekindicc  15444  plyco  15570  isclwwlk  16335  clwwlknon2x  16376  iseupthf1o  16389  2omap  16715