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  2779  ceqsex4v  2780  ceqsex8v  2782  reu2  2925  reu6  2926  reu4  2931  reu7  2932  rmo3f  2934  rmo4f  2935  2rmorex  2943  rmo3  3054  raldifb  3275  inass  3345  dfss4st  3368  ssddif  3369  difin  3372  invdif  3377  indif  3378  indi  3382  difundi  3387  difindiss  3389  inssdif0im  3490  rexdifpr  3620  ssdifsn  3720  unipr  3823  uniun  3828  uniin  3829  iunin2  3950  iindif2m  3954  iinin2m  3955  elpwpw  3973  unidif0  4167  mss  4226  eqvinop  4243  opcom  4250  opeqsn  4252  uniuni  4451  zfinf2  4588  elomssom  4604  fconstmpt  4673  opeliunxp  4681  xpundi  4682  elvvv  4689  xpiindim  4764  elcnv2  4805  cnvuni  4813  dmuni  4837  opelres  4912  restidsing  4963  elima3  4977  imai  4984  imainss  5044  ssrnres  5071  cnvresima  5118  mptpreima  5122  coundir  5131  rnco  5135  coass  5147  relrelss  5155  dffun2  5226  dffun4  5227  dffun6f  5229  dffun4f  5232  dffun7  5243  dffun8  5244  dffun9  5245  svrelfun  5281  fncnv  5282  funcnvuni  5285  dfmpt3  5338  fintm  5401  fin  5402  dff12  5420  fores  5447  dff1o4  5469  eqfnfv3  5615  unpreima  5641  ffnfvf  5675  dff13f  5770  ffnov  5978  eqfnov  5980  foov  6020  opabex3d  6121  opabex3  6122  mpoxopovel  6241  tpostpos  6264  dfsmo2  6287  tfr1onlemaccex  6348  tfrcllembxssdm  6356  tfrcllemaccex  6361  tfrcllemres  6362  tfrcldm  6363  erinxp  6608  mapsncnv  6694  cbvixp  6714  ixpin  6722  ixpiinm  6723  mptelixpg  6733  elixpsn  6734  ixpsnf1o  6735  mapsnen  6810  xpassen  6829  2omotaplemap  7255  distrnqg  7385  subhalfnqq  7412  enq0enq  7429  enq0sym  7430  enq0tr  7432  addnq0mo  7445  mulnq0mo  7446  distrnq0  7457  prarloc  7501  nqprrnd  7541  ltexprlemopl  7599  ltexprlemlol  7600  ltexprlemopu  7601  ltexprlemupu  7602  ltexprlemdisj  7604  ltexprlemloc  7605  recexprlemdisj  7628  caucvgprprlemell  7683  caucvgprprlemelu  7684  addsrmo  7741  mulsrmo  7742  opelreal  7825  axcaucvglemres  7897  axpre-suploc  7900  elnnz  9262  elznn0nn  9266  zltlen  9330  suprzclex  9350  peano2uz2  9359  peano5uzti  9360  qltlen  9639  elfzuzb  10018  4fvwrd4  10139  fzind2  10238  cvg1nlemres  10993  rexfiuz  10997  cbvsum  11367  mertenslem2  11543  mertensabs  11544  cbvprod  11565  prodmodc  11585  fprodseq  11590  ndvdssub  11934  nnwosdc  12039  isprm2  12116  isprm4  12118  hashdvds  12220  xpscf  12765  isnsg2  13061  isnsg4  13070  subsubrg2  13365  isbasis2g  13515  tgval2  13521  elcncf1di  14036  dedekindicclemicc  14080  dedekindicc  14081