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  4212  mss  4271  eqvinop  4288  opcom  4296  opeqsn  4298  uniuni  4499  zfinf2  4638  elomssom  4654  fconstmpt  4723  opeliunxp  4731  xpundi  4732  elvvv  4739  xpiindim  4816  elcnv2  4857  cnvuni  4865  dmuni  4889  opelres  4965  restidsing  5016  elima3  5030  imai  5039  imainss  5099  ssrnres  5126  cnvresima  5173  mptpreima  5177  coundir  5186  rnco  5190  coass  5202  relrelss  5210  dffun2  5282  dffun4  5283  dffun6f  5285  dffun4f  5288  dffun7  5299  dffun8  5300  dffun9  5301  svrelfun  5340  fncnv  5341  funcnvuni  5344  dfmpt3  5400  fintm  5463  fin  5464  dff12  5482  fores  5510  dff1o4  5532  eqfnfv3  5681  unpreima  5707  ffnfvf  5741  dff13f  5841  ffnov  6051  eqfnov  6054  foov  6095  opabex3d  6208  opabex3  6209  uchoice  6225  mpoxopovel  6329  tpostpos  6352  dfsmo2  6375  tfr1onlemaccex  6436  tfrcllembxssdm  6444  tfrcllemaccex  6449  tfrcllemres  6450  tfrcldm  6451  erinxp  6698  mapsncnv  6784  cbvixp  6804  ixpin  6812  ixpiinm  6813  mptelixpg  6823  elixpsn  6824  ixpsnf1o  6825  mapsnen  6905  xpassen  6927  2omotaplemap  7371  distrnqg  7502  subhalfnqq  7529  enq0enq  7546  enq0sym  7547  enq0tr  7549  addnq0mo  7562  mulnq0mo  7563  distrnq0  7574  prarloc  7618  nqprrnd  7658  ltexprlemopl  7716  ltexprlemlol  7717  ltexprlemopu  7718  ltexprlemupu  7719  ltexprlemdisj  7721  ltexprlemloc  7722  recexprlemdisj  7745  caucvgprprlemell  7800  caucvgprprlemelu  7801  addsrmo  7858  mulsrmo  7859  opelreal  7942  axcaucvglemres  8014  axpre-suploc  8017  elnnz  9384  elznn0nn  9388  zltlen  9453  suprzclex  9473  peano2uz2  9482  peano5uzti  9483  qltlen  9763  elfzuzb  10143  4fvwrd4  10264  fzind2  10370  cvg1nlemres  11329  rexfiuz  11333  cbvsum  11704  mertenslem2  11880  mertensabs  11881  cbvprod  11902  prodmodc  11922  fprodseq  11927  ndvdssub  12274  bitsmod  12300  nnwosdc  12393  isprm2  12472  isprm4  12474  hashdvds  12576  xpscf  13212  fngsum  13253  igsumvalx  13254  isnsg2  13572  isnsg4  13581  isrhm  13953  issubrng  13994  subsubrng2  14010  subsubrg2  14041  isbasis2g  14550  tgval2  14556  elcncf1di  15084  dedekindicclemicc  15137  dedekindicc  15138  plyco  15264  2omap  15969