Theorem anbi2i 461

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

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi12i  464  bianass  473  mpan10  478  an4  592  an42  593  anandir  599  dcim  853  19.27h  1613  19.27  1614  19.41  1738  sbcof2  1863  sbidm  1904  sb6  1941  3exdistr  1971  4exdistr  1972  2sb5  2043  2sb5rf  2049  sbel2x  2058  eu2  2131  euan  2143  sbmo  2146  mo4f  2147  eu4  2149  moanim  2161  2eu4  2180  clelab  2366  nonconne  2432  r2exf  2568  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  reu2  3014  reu6  3015  reu4  3020  reu7  3021  rmo3f  3023  rmo4f  3024  2rmorex  3032  rmo3  3144  raldifb  3369  inass  3441  dfss4st  3464  ssddif  3465  difin  3468  invdif  3473  indif  3474  indi  3478  difundi  3483  difindiss  3485  inssdif0imOLD  3593  rexdifpr  3737  ssdifsn  3842  unipr  3949  uniun  3954  uniin  3955  iunin2  4076  iindif2m  4080  iinin2m  4081  elpwpw  4099  unidif0  4304  mss  4366  eqvinop  4383  opcom  4391  opeqsn  4393  uniuni  4597  zfinf2  4736  elomssom  4752  fconstmpt  4822  opeliunxp  4830  xpundi  4831  elvvv  4838  xpiindim  4917  elcnv2  4958  cnvuni  4966  dmuni  4991  opelres  5068  restidsing  5119  elima3  5133  imai  5143  imainss  5203  ssrnres  5230  cnvresima  5277  mptpreima  5281  coundir  5290  rnco  5294  coass  5306  relrelss  5314  dffun2  5387  dffun4  5388  dffun6f  5390  dffun4f  5393  dffun7  5404  dffun8  5405  dffun9  5406  svrelfun  5446  fncnv  5447  funcnvuni  5450  dfmpt3  5506  fintm  5577  fin  5578  dff12  5597  fores  5625  dff1o4  5647  eqfnfv3  5808  unpreima  5833  ffnfvf  5867  dff13f  5976  ffnov  6192  eqfnov  6195  foov  6236  opabex3d  6350  opabex3  6351  uchoice  6371  mpoxopovel  6512  tpostpos  6535  dfsmo2  6558  tfr1onlemaccex  6619  tfrcllembxssdm  6627  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  erinxp  6883  mapsncnv  6977  cbvixp  6997  ixpin  7005  ixpiinm  7006  mptelixpg  7016  elixpsn  7017  ixpsnf1o  7018  mapsnen  7100  xpassen  7128  2omap  7318  2omotaplemap  7623  distrnqg  7754  subhalfnqq  7781  enq0enq  7798  enq0sym  7799  enq0tr  7801  addnq0mo  7814  mulnq0mo  7815  distrnq0  7826  prarloc  7870  nqprrnd  7910  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemdisj  7973  ltexprlemloc  7974  recexprlemdisj  7997  caucvgprprlemell  8052  caucvgprprlemelu  8053  addsrmo  8110  mulsrmo  8111  opelreal  8194  axcaucvglemres  8266  axpre-suploc  8269  elnnz  9654  elznn0nn  9658  zltlen  9724  suprzclex  9744  peano2uz2  9753  peano5uzti  9754  qltlen  10040  elfzuzb  10422  4fvwrd4  10547  fzind2  10658  cvg1nlemres  11751  rexfiuz  11755  cbvsum  12126  mertenslem2  12303  mertensabs  12304  cbvprod  12325  prodmodc  12345  fprodseq  12350  ndvdssub  12697  bitsmod  12723  nnwosdc  12816  isprm2  12895  isprm4  12897  hashdvds  12999  xpscf  13668  fngzsum  13708  gzsumvalx  13709  isnsg2  14006  isnsg4  14015  isrhm  14465  issubrng  14507  subsubrng2  14523  subsubrg2  14554  isbasis2g  15146  tgval2  15152  elcncf1di  15680  dedekindicclemicc  15733  dedekindicc  15734  plyco  15860  isclwwlk  16635  clwwlknon2x  16676  iseupthf1o  16689  alsanmo  17151  ralsanmo  17152  2alsraln0m  17158  2alsraln0idm  17159