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  593  dcim  846  19.27h  1606  19.27  1607  19.41  1732  sbcof2  1856  sbidm  1897  sb6  1933  3exdistr  1962  4exdistr  1963  2sb5  2034  2sb5rf  2040  sbel2x  2049  eu2  2122  euan  2134  sbmo  2137  mo4f  2138  eu4  2140  moanim  2152  2eu4  2171  clelab  2355  nonconne  2412  r2exf  2548  ceqsex3v  2843  ceqsex4v  2844  ceqsex8v  2846  reu2  2991  reu6  2992  reu4  2997  reu7  2998  rmo3f  3000  rmo4f  3001  2rmorex  3009  rmo3  3121  raldifb  3344  inass  3414  dfss4st  3437  ssddif  3438  difin  3441  invdif  3446  indif  3447  indi  3451  difundi  3456  difindiss  3458  inssdif0im  3559  rexdifpr  3694  ssdifsn  3796  unipr  3902  uniun  3907  uniin  3908  iunin2  4029  iindif2m  4033  iinin2m  4034  elpwpw  4052  unidif0  4251  mss  4312  eqvinop  4329  opcom  4337  opeqsn  4339  uniuni  4542  zfinf2  4681  elomssom  4697  fconstmpt  4766  opeliunxp  4774  xpundi  4775  elvvv  4782  xpiindim  4859  elcnv2  4900  cnvuni  4908  dmuni  4933  opelres  5010  restidsing  5061  elima3  5075  imai  5084  imainss  5144  ssrnres  5171  cnvresima  5218  mptpreima  5222  coundir  5231  rnco  5235  coass  5247  relrelss  5255  dffun2  5328  dffun4  5329  dffun6f  5331  dffun4f  5334  dffun7  5345  dffun8  5346  dffun9  5347  svrelfun  5386  fncnv  5387  funcnvuni  5390  dfmpt3  5446  fintm  5511  fin  5512  dff12  5530  fores  5558  dff1o4  5580  eqfnfv3  5734  unpreima  5760  ffnfvf  5794  dff13f  5894  ffnov  6108  eqfnov  6111  foov  6152  opabex3d  6266  opabex3  6267  uchoice  6283  mpoxopovel  6387  tpostpos  6410  dfsmo2  6433  tfr1onlemaccex  6494  tfrcllembxssdm  6502  tfrcllemaccex  6507  tfrcllemres  6508  tfrcldm  6509  erinxp  6756  mapsncnv  6842  cbvixp  6862  ixpin  6870  ixpiinm  6871  mptelixpg  6881  elixpsn  6882  ixpsnf1o  6883  mapsnen  6964  xpassen  6989  2omotaplemap  7443  distrnqg  7574  subhalfnqq  7601  enq0enq  7618  enq0sym  7619  enq0tr  7621  addnq0mo  7634  mulnq0mo  7635  distrnq0  7646  prarloc  7690  nqprrnd  7730  ltexprlemopl  7788  ltexprlemlol  7789  ltexprlemopu  7790  ltexprlemupu  7791  ltexprlemdisj  7793  ltexprlemloc  7794  recexprlemdisj  7817  caucvgprprlemell  7872  caucvgprprlemelu  7873  addsrmo  7930  mulsrmo  7931  opelreal  8014  axcaucvglemres  8086  axpre-suploc  8089  elnnz  9456  elznn0nn  9460  zltlen  9525  suprzclex  9545  peano2uz2  9554  peano5uzti  9555  qltlen  9835  elfzuzb  10215  4fvwrd4  10336  fzind2  10445  cvg1nlemres  11496  rexfiuz  11500  cbvsum  11871  mertenslem2  12047  mertensabs  12048  cbvprod  12069  prodmodc  12089  fprodseq  12094  ndvdssub  12441  bitsmod  12467  nnwosdc  12560  isprm2  12639  isprm4  12641  hashdvds  12743  xpscf  13380  fngsum  13421  igsumvalx  13422  isnsg2  13740  isnsg4  13749  isrhm  14122  issubrng  14163  subsubrng2  14179  subsubrg2  14210  isbasis2g  14719  tgval2  14725  elcncf1di  15253  dedekindicclemicc  15306  dedekindicc  15307  plyco  15433  2omap  16359