Theorem anbi2i 452

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi12i  455  mpan10  465  an4  575  an42  576  anandir  580  dcim  826  19.27h  1539  19.27  1540  19.41  1664  sbcof2  1782  sbidm  1823  sb6  1858  3exdistr  1887  4exdistr  1888  2sb5  1956  2sb5rf  1962  sbel2x  1971  eu2  2041  euan  2053  sbmo  2056  mo4f  2057  eu4  2059  moanim  2071  2eu4  2090  clelab  2263  nonconne  2318  r2exf  2451  ceqsex3v  2723  ceqsex4v  2724  ceqsex8v  2726  reu2  2867  reu6  2868  reu4  2873  reu7  2874  rmo3f  2876  rmo4f  2877  2rmorex  2885  rmo3  2995  raldifb  3211  inass  3281  dfss4st  3304  ssddif  3305  difin  3308  invdif  3313  indif  3314  indi  3318  difundi  3323  difindiss  3325  inssdif0im  3425  ssdifsn  3646  unipr  3745  uniun  3750  uniin  3751  iunin2  3871  iindif2m  3875  iinin2m  3876  elpwpw  3894  unidif0  4086  mss  4143  eqvinop  4160  opcom  4167  opeqsn  4169  uniuni  4367  zfinf2  4498  elnn  4514  fconstmpt  4581  opeliunxp  4589  xpundi  4590  elvvv  4597  xpiindim  4671  elcnv2  4712  cnvuni  4720  dmuni  4744  opelres  4819  elima3  4883  imai  4890  imainss  4949  ssrnres  4976  cnvresima  5023  mptpreima  5027  coundir  5036  rnco  5040  coass  5052  relrelss  5060  dffun2  5128  dffun4  5129  dffun6f  5131  dffun4f  5134  dffun7  5145  dffun8  5146  dffun9  5147  svrelfun  5183  fncnv  5184  funcnvuni  5187  dfmpt3  5240  fintm  5303  fin  5304  dff12  5322  fores  5349  dff1o4  5368  eqfnfv3  5513  unpreima  5538  ffnfvf  5572  dff13f  5664  ffnov  5868  eqfnov  5870  foov  5910  opabex3d  6012  opabex3  6013  mpoxopovel  6131  tpostpos  6154  dfsmo2  6177  tfr1onlemaccex  6238  tfrcllembxssdm  6246  tfrcllemaccex  6251  tfrcllemres  6252  tfrcldm  6253  erinxp  6496  mapsncnv  6582  cbvixp  6602  ixpin  6610  ixpiinm  6611  mptelixpg  6621  elixpsn  6622  ixpsnf1o  6623  mapsnen  6698  xpassen  6717  distrnqg  7188  subhalfnqq  7215  enq0enq  7232  enq0sym  7233  enq0tr  7235  addnq0mo  7248  mulnq0mo  7249  distrnq0  7260  prarloc  7304  nqprrnd  7344  ltexprlemopl  7402  ltexprlemlol  7403  ltexprlemopu  7404  ltexprlemupu  7405  ltexprlemdisj  7407  ltexprlemloc  7408  recexprlemdisj  7431  caucvgprprlemell  7486  caucvgprprlemelu  7487  addsrmo  7544  mulsrmo  7545  opelreal  7628  axcaucvglemres  7700  axpre-suploc  7703  elnnz  9057  elznn0nn  9061  zltlen  9122  suprzclex  9142  peano2uz2  9151  peano5uzti  9152  qltlen  9425  elfzuzb  9793  4fvwrd4  9910  fzind2  10009  cvg1nlemres  10750  rexfiuz  10754  cbvsum  11122  mertenslem2  11298  mertensabs  11299  cbvprod  11320  ndvdssub  11616  isprm2  11787  isprm4  11789  hashdvds  11886  isbasis2g  12201  tgval2  12209  elcncf1di  12724  dedekindicclemicc  12768  dedekindicc  12769