Theorem anbi2i 445

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anbi12i  448  mpan10  458  an4  551  an42  552  anandir  556  dcim  818  19.27h  1493  19.27  1494  19.41  1617  sbcof2  1732  sbidm  1773  sb6  1808  3exdistr  1834  4exdistr  1835  2sb5  1901  2sb5rf  1907  sbel2x  1916  eu2  1986  euan  1998  sbmo  2001  mo4f  2002  eu4  2004  moanim  2016  2eu4  2035  clelab  2204  nonconne  2258  r2exf  2385  ceqsex3v  2642  ceqsex4v  2643  ceqsex8v  2645  reu2  2781  reu6  2782  reu4  2787  reu7  2788  2rmorex  2797  rmo3  2906  raldifb  3113  inass  3183  ssddif  3205  difin  3208  invdif  3213  indif  3214  indi  3218  difundi  3223  difindiss  3225  inssdif0im  3318  unipr  3623  uniun  3628  uniin  3629  iunin2  3749  iindif2m  3753  iinin2m  3754  unidif0  3949  mss  3989  eqvinop  4006  opcom  4013  opeqsn  4015  uniuni  4209  zfinf2  4338  elnn  4354  fconstmpt  4413  opeliunxp  4421  xpundi  4422  elvvv  4429  xpiindim  4501  elcnv2  4541  cnvuni  4549  dmuni  4573  opelres  4645  elima3  4705  imai  4711  imainss  4769  ssrnres  4793  cnvresima  4840  mptpreima  4844  coundir  4853  rnco  4857  coass  4869  relrelss  4874  dffun2  4942  dffun4  4943  dffun6f  4945  dffun4f  4948  dffun7  4958  dffun8  4959  dffun9  4960  svrelfun  4995  fncnv  4996  funcnvuni  4999  dfmpt3  5052  fintm  5106  fin  5107  dff12  5122  fores  5146  dff1o4  5165  eqfnfv3  5299  unpreima  5324  ffnfvf  5356  dff13f  5441  ffnov  5636  eqfnov  5638  foov  5678  opabex3d  5779  opabex3  5780  mpt2xopovel  5890  tpostpos  5913  dfsmo2  5936  tfr1onlemaccex  5997  tfrcllembxssdm  6005  tfrcllemaccex  6010  tfrcllemres  6011  tfrcldm  6012  erinxp  6246  xpassen  6374  distrnqg  6639  subhalfnqq  6666  enq0enq  6683  enq0sym  6684  enq0tr  6686  addnq0mo  6699  mulnq0mo  6700  distrnq0  6711  prarloc  6755  nqprrnd  6795  ltexprlemopl  6853  ltexprlemlol  6854  ltexprlemopu  6855  ltexprlemupu  6856  ltexprlemdisj  6858  ltexprlemloc  6859  recexprlemdisj  6882  caucvgprprlemell  6937  caucvgprprlemelu  6938  addsrmo  6982  mulsrmo  6983  opelreal  7058  axcaucvglemres  7127  elnnz  8442  elznn0nn  8446  zltlen  8507  suprzclex  8526  peano2uz2  8535  peano5uzti  8536  qltlen  8806  elfzuzb  9115  4fvwrd4  9227  fzind2  9325  cvg1nlemres  10009  rexfiuz  10013  ndvdssub  10474  isprm2  10643  isprm4  10645