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  2781  ceqsex4v  2782  ceqsex8v  2784  reu2  2927  reu6  2928  reu4  2933  reu7  2934  rmo3f  2936  rmo4f  2937  2rmorex  2945  rmo3  3056  raldifb  3277  inass  3347  dfss4st  3370  ssddif  3371  difin  3374  invdif  3379  indif  3380  indi  3384  difundi  3389  difindiss  3391  inssdif0im  3492  rexdifpr  3622  ssdifsn  3722  unipr  3825  uniun  3830  uniin  3831  iunin2  3952  iindif2m  3956  iinin2m  3957  elpwpw  3975  unidif0  4169  mss  4228  eqvinop  4245  opcom  4252  opeqsn  4254  uniuni  4453  zfinf2  4590  elomssom  4606  fconstmpt  4675  opeliunxp  4683  xpundi  4684  elvvv  4691  xpiindim  4766  elcnv2  4807  cnvuni  4815  dmuni  4839  opelres  4914  restidsing  4965  elima3  4979  imai  4986  imainss  5046  ssrnres  5073  cnvresima  5120  mptpreima  5124  coundir  5133  rnco  5137  coass  5149  relrelss  5157  dffun2  5228  dffun4  5229  dffun6f  5231  dffun4f  5234  dffun7  5245  dffun8  5246  dffun9  5247  svrelfun  5283  fncnv  5284  funcnvuni  5287  dfmpt3  5340  fintm  5403  fin  5404  dff12  5422  fores  5449  dff1o4  5471  eqfnfv3  5618  unpreima  5644  ffnfvf  5678  dff13f  5774  ffnov  5982  eqfnov  5984  foov  6024  opabex3d  6125  opabex3  6126  mpoxopovel  6245  tpostpos  6268  dfsmo2  6291  tfr1onlemaccex  6352  tfrcllembxssdm  6360  tfrcllemaccex  6365  tfrcllemres  6366  tfrcldm  6367  erinxp  6612  mapsncnv  6698  cbvixp  6718  ixpin  6726  ixpiinm  6727  mptelixpg  6737  elixpsn  6738  ixpsnf1o  6739  mapsnen  6814  xpassen  6833  2omotaplemap  7259  distrnqg  7389  subhalfnqq  7416  enq0enq  7433  enq0sym  7434  enq0tr  7436  addnq0mo  7449  mulnq0mo  7450  distrnq0  7461  prarloc  7505  nqprrnd  7545  ltexprlemopl  7603  ltexprlemlol  7604  ltexprlemopu  7605  ltexprlemupu  7606  ltexprlemdisj  7608  ltexprlemloc  7609  recexprlemdisj  7632  caucvgprprlemell  7687  caucvgprprlemelu  7688  addsrmo  7745  mulsrmo  7746  opelreal  7829  axcaucvglemres  7901  axpre-suploc  7904  elnnz  9266  elznn0nn  9270  zltlen  9334  suprzclex  9354  peano2uz2  9363  peano5uzti  9364  qltlen  9643  elfzuzb  10022  4fvwrd4  10143  fzind2  10242  cvg1nlemres  10997  rexfiuz  11001  cbvsum  11371  mertenslem2  11547  mertensabs  11548  cbvprod  11569  prodmodc  11589  fprodseq  11594  ndvdssub  11938  nnwosdc  12043  isprm2  12120  isprm4  12122  hashdvds  12224  xpscf  12773  isnsg2  13077  isnsg4  13086  subsubrg2  13405  isbasis2g  13733  tgval2  13739  elcncf1di  14254  dedekindicclemicc  14298  dedekindicc  14299