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  4199  unidif0  4211  bnd2  4217  otth2  4285  copsexg  4288  copsex4g  4291  opeqsn  4297  opelopabsbALT  4305  elpwpwel  4522  suc11g  4605  rabxp  4712  opeliunxp  4730  xpundir  4732  xpiundi  4733  xpiundir  4734  brinxp2  4742  rexiunxp  4820  brres  4965  brresg  4967  dmres  4980  resiexg  5004  dminss  5097  imainss  5098  ssrnres  5125  elxp4  5170  elxp5  5171  cnvresima  5172  coundi  5184  resco  5187  imaco  5188  coiun  5192  coi1  5198  coass  5201  xpcom  5229  dffun2  5281  fncnv  5340  imadiflem  5353  imadif  5354  imainlem  5355  mptun  5407  fcnvres  5459  dff1o2  5527  dff1o3  5528  ffoss  5554  f11o  5555  brprcneu  5569  fvun2  5646  eqfnfv3  5679  respreima  5708  f1ompt  5731  fsn  5752  abrexco  5828  imaiun  5829  f1mpt  5840  dff1o6  5845  oprabid  5976  dfoprab2  5992  oprab4  6016  mpomptx  6036  opabex3d  6206  opabex3  6207  abexssex  6210  dfopab2  6275  dfoprab3s  6276  1stconst  6307  2ndconst  6308  xporderlem  6317  spc2ed  6319  f1od2  6321  brtpos2  6337  tpostpos  6350  tposmpo  6367  oviec  6728  mapsncnv  6782  dfixp  6787  domen  6840  mapsnen  6903  xpsnen  6916  xpcomco  6921  xpassen  6925  ltexpi  7450  dfmq0qs  7542  dfplq0qs  7543  enq0enq  7544  enq0ref  7546  enq0tr  7547  nqnq0pi  7551  prnmaxl  7601  prnminu  7602  suplocexprlemloc  7834  addsrpr  7858  mulsrpr  7859  suplocsrlemb  7919  addcnsr  7947  mulcnsr  7948  ltresr  7952  addvalex  7957  axprecex  7993  elnnz  9382  fnn0ind  9489  rexuz2  9702  qreccl  9763  rexrp  9798  elixx3g  10023  elfz2  10137  elfzuzb  10141  fznn  10211  elfz2nn0  10234  fznn0  10235  4fvwrd4  10262  elfzo2  10272  fzind2  10368  cvg1nlemres  11296  fsum2dlemstep  11745  modfsummod  11769  fprodseq  11894  divalgb  12236  bezoutlemmain  12319  isprm2  12439  oddpwdc  12496  prdsex  13101  prdsval  13105  prdsbaslemss  13106  xpscf  13179  issubg3  13528  releqgg  13556  eqgex  13557  imasabl  13672  dfrhm2  13916  ntreq0  14604  cnnei  14704  txlm  14751  blres  14906  isms2  14926  dedekindicclemicc  15104  limcrcl  15130  lgsquadlem1  15554  lgsquadlem2  15555  bdcriota  15819  bj-peano4  15891  alsconv  16019