Theorem anbi1i 458

Description: Introduce a right 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
anbi1i	|- ( ( ph /\ ch ) <-> ( ps /\ ch ) )

Proof of Theorem anbi1i

Step	Hyp	Ref	Expression
1		bi.aa	. . 3 |- ( ph <-> ps )
2	1	a1i 9	. 2 |- ( ch -> ( ph <-> ps ) )
3	2	pm5.32ri 455	1 |- ( ( ph /\ ch ) <-> ( ps /\ ch ) )

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:  anbi2ci  459  anbi12i  460  bianassc  470  an12  561  anandi  590  pm5.53  804  pm5.75  965  3ancoma  988  3ioran  996  an6  1334  19.26-3an  1506  19.28h  1585  19.28  1586  eeeanv  1961  sb3an  1986  moanim  2128  nfrexdya  2542  r19.26-3  2636  r19.41  2661  rexcomf  2668  3reeanv  2677  cbvreu  2736  ceqsex3v  2815  rexab  2935  rexrab  2936  rmo4  2966  rmo3f  2970  reuind  2978  sbc3an  3060  rmo3  3090  ssrab  3271  rexun  3353  elin3  3364  inass  3383  unssdif  3408  indifdir  3429  difin2  3435  inrab2  3446  rabun2  3452  reuun2  3456  undif4  3523  rexdifpr  3661  rexsns  3672  rexdifsn  3765  2ralunsn  3839  iuncom4  3934  iunxiun  4009  inuni  4200  unidif0  4212  bnd2  4218  otth2  4286  copsexg  4289  copsex4g  4292  opeqsn  4298  opelopabsbALT  4306  elpwpwel  4523  suc11g  4606  rabxp  4713  opeliunxp  4731  xpundir  4733  xpiundi  4734  xpiundir  4735  brinxp2  4743  rexiunxp  4821  brres  4966  brresg  4968  dmres  4981  resiexg  5005  dminss  5098  imainss  5099  ssrnres  5126  elxp4  5171  elxp5  5172  cnvresima  5173  coundi  5185  resco  5188  imaco  5189  coiun  5193  coi1  5199  coass  5202  xpcom  5230  dffun2  5282  fncnv  5341  imadiflem  5354  imadif  5355  imainlem  5356  mptun  5409  fcnvres  5461  dff1o2  5529  dff1o3  5530  ffoss  5556  f11o  5557  brprcneu  5571  fvun2  5648  eqfnfv3  5681  respreima  5710  f1ompt  5733  fsn  5754  abrexco  5830  imaiun  5831  f1mpt  5842  dff1o6  5847  oprabid  5978  dfoprab2  5994  oprab4  6018  mpomptx  6038  opabex3d  6208  opabex3  6209  abexssex  6212  dfopab2  6277  dfoprab3s  6278  1stconst  6309  2ndconst  6310  xporderlem  6319  spc2ed  6321  f1od2  6323  brtpos2  6339  tpostpos  6352  tposmpo  6369  oviec  6730  mapsncnv  6784  dfixp  6789  domen  6842  mapsnen  6905  xpsnen  6918  xpcomco  6923  xpassen  6927  ltexpi  7452  dfmq0qs  7544  dfplq0qs  7545  enq0enq  7546  enq0ref  7548  enq0tr  7549  nqnq0pi  7553  prnmaxl  7603  prnminu  7604  suplocexprlemloc  7836  addsrpr  7860  mulsrpr  7861  suplocsrlemb  7921  addcnsr  7949  mulcnsr  7950  ltresr  7954  addvalex  7959  axprecex  7995  elnnz  9384  fnn0ind  9491  rexuz2  9704  qreccl  9765  rexrp  9800  elixx3g  10025  elfz2  10139  elfzuzb  10143  fznn  10213  elfz2nn0  10236  fznn0  10237  4fvwrd4  10264  elfzo2  10274  fzind2  10370  cvg1nlemres  11329  fsum2dlemstep  11778  modfsummod  11802  fprodseq  11927  divalgb  12269  bezoutlemmain  12352  isprm2  12472  oddpwdc  12529  prdsex  13134  prdsval  13138  prdsbaslemss  13139  xpscf  13212  issubg3  13561  releqgg  13589  eqgex  13590  imasabl  13705  dfrhm2  13949  ntreq0  14637  cnnei  14737  txlm  14784  blres  14939  isms2  14959  dedekindicclemicc  15137  limcrcl  15163  lgsquadlem1  15587  lgsquadlem2  15588  bdcriota  15856  bj-peano4  15928  alsconv  16056