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  1584  19.27  1585  19.41  1710  sbcof2  1834  sbidm  1875  sb6  1911  3exdistr  1940  4exdistr  1941  2sb5  2012  2sb5rf  2018  sbel2x  2027  eu2  2100  euan  2112  sbmo  2115  mo4f  2116  eu4  2118  moanim  2130  2eu4  2149  clelab  2333  nonconne  2390  r2exf  2526  ceqsex3v  2820  ceqsex4v  2821  ceqsex8v  2823  reu2  2968  reu6  2969  reu4  2974  reu7  2975  rmo3f  2977  rmo4f  2978  2rmorex  2986  rmo3  3098  raldifb  3321  inass  3391  dfss4st  3414  ssddif  3415  difin  3418  invdif  3423  indif  3424  indi  3428  difundi  3433  difindiss  3435  inssdif0im  3536  rexdifpr  3671  ssdifsn  3772  unipr  3878  uniun  3883  uniin  3884  iunin2  4005  iindif2m  4009  iinin2m  4010  elpwpw  4028  unidif0  4227  mss  4288  eqvinop  4305  opcom  4313  opeqsn  4315  uniuni  4516  zfinf2  4655  elomssom  4671  fconstmpt  4740  opeliunxp  4748  xpundi  4749  elvvv  4756  xpiindim  4833  elcnv2  4874  cnvuni  4882  dmuni  4907  opelres  4983  restidsing  5034  elima3  5048  imai  5057  imainss  5117  ssrnres  5144  cnvresima  5191  mptpreima  5195  coundir  5204  rnco  5208  coass  5220  relrelss  5228  dffun2  5300  dffun4  5301  dffun6f  5303  dffun4f  5306  dffun7  5317  dffun8  5318  dffun9  5319  svrelfun  5358  fncnv  5359  funcnvuni  5362  dfmpt3  5418  fintm  5483  fin  5484  dff12  5502  fores  5530  dff1o4  5552  eqfnfv3  5702  unpreima  5728  ffnfvf  5762  dff13f  5862  ffnov  6072  eqfnov  6075  foov  6116  opabex3d  6229  opabex3  6230  uchoice  6246  mpoxopovel  6350  tpostpos  6373  dfsmo2  6396  tfr1onlemaccex  6457  tfrcllembxssdm  6465  tfrcllemaccex  6470  tfrcllemres  6471  tfrcldm  6472  erinxp  6719  mapsncnv  6805  cbvixp  6825  ixpin  6833  ixpiinm  6834  mptelixpg  6844  elixpsn  6845  ixpsnf1o  6846  mapsnen  6927  xpassen  6950  2omotaplemap  7404  distrnqg  7535  subhalfnqq  7562  enq0enq  7579  enq0sym  7580  enq0tr  7582  addnq0mo  7595  mulnq0mo  7596  distrnq0  7607  prarloc  7651  nqprrnd  7691  ltexprlemopl  7749  ltexprlemlol  7750  ltexprlemopu  7751  ltexprlemupu  7752  ltexprlemdisj  7754  ltexprlemloc  7755  recexprlemdisj  7778  caucvgprprlemell  7833  caucvgprprlemelu  7834  addsrmo  7891  mulsrmo  7892  opelreal  7975  axcaucvglemres  8047  axpre-suploc  8050  elnnz  9417  elznn0nn  9421  zltlen  9486  suprzclex  9506  peano2uz2  9515  peano5uzti  9516  qltlen  9796  elfzuzb  10176  4fvwrd4  10297  fzind2  10405  cvg1nlemres  11411  rexfiuz  11415  cbvsum  11786  mertenslem2  11962  mertensabs  11963  cbvprod  11984  prodmodc  12004  fprodseq  12009  ndvdssub  12356  bitsmod  12382  nnwosdc  12475  isprm2  12554  isprm4  12556  hashdvds  12658  xpscf  13294  fngsum  13335  igsumvalx  13336  isnsg2  13654  isnsg4  13663  isrhm  14035  issubrng  14076  subsubrng2  14092  subsubrg2  14123  isbasis2g  14632  tgval2  14638  elcncf1di  15166  dedekindicclemicc  15219  dedekindicc  15220  plyco  15346  2omap  16132