Theorem anbi1i 462

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

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi2ci  463  anbi12i  464  bianassc  474  an12  567  anandi  598  pm5.53  814  pm5.75  975  3ancoma  1016  3ioran  1024  an6  1362  19.26-3an  1536  19.28h  1615  19.28  1616  eeeanv  1993  sb3an  2018  moanim  2161  nfrexdya  2586  r19.26-3  2681  r19.41  2706  rexcomf  2713  3reeanv  2722  cbvreu  2784  ceqsex3v  2865  rexab  2988  rexrab  2989  rmo4  3019  rmo3f  3023  reuind  3031  sbc3an  3113  rmo3  3144  ssrab  3326  rexun  3409  elin3  3420  inass  3441  unssdif  3466  indifdir  3487  difin2  3493  inrab2  3506  rabun2  3512  reuun2  3516  undif4  3587  rexdifpr  3737  rexsns  3748  rexdifsn  3846  2ralunsn  3924  iuncom4  4019  iunxiun  4094  inuni  4291  unidif0  4304  bnd2  4310  otth2  4381  copsexg  4384  copsex4g  4387  opeqsn  4393  opelopabsbALT  4401  elpwpwel  4621  suc11g  4704  rabxp  4812  opeliunxp  4830  xpundir  4832  xpiundi  4833  xpiundir  4834  brinxp2  4842  rexiunxp  4922  brres  5069  brresg  5071  dmres  5084  resiexg  5108  dminss  5202  imainss  5203  ssrnres  5230  elxp4  5275  elxp5  5276  cnvresima  5277  coundi  5289  resco  5292  imaco  5293  coiun  5297  coi1  5303  coass  5306  xpcom  5334  dffun2  5387  fncnv  5447  imadiflem  5460  imadif  5461  imainlem  5462  mptun  5515  fcnvres  5575  dff1o2  5644  dff1o3  5645  ffoss  5672  f11o  5673  brprcneu  5688  fvun2  5770  eqfnfv3  5808  respreima  5836  f1ompt  5859  fsn  5880  abrexco  5965  imaiun  5966  f1mpt  5977  dff1o6  5982  oprabid  6117  dfoprab2  6135  oprab4  6159  mpomptx  6179  opabex3d  6350  opabex3  6351  abexssex  6354  dfopab2  6423  dfoprab3s  6424  1stconst  6457  2ndconst  6458  xporderlem  6467  spc2ed  6469  f1od2  6471  brtpos2  6522  tpostpos  6535  tposmpo  6552  oviec  6915  mapsncnv  6977  dfixp  6982  domen  7035  mapsnen  7100  xpsnen  7119  xpcomco  7124  xpassen  7128  sspw1or2  7544  ltexpi  7704  dfmq0qs  7796  dfplq0qs  7797  enq0enq  7798  enq0ref  7800  enq0tr  7801  nqnq0pi  7805  prnmaxl  7855  prnminu  7856  suplocexprlemloc  8088  addsrpr  8112  mulsrpr  8113  suplocsrlemb  8173  addcnsr  8201  mulcnsr  8202  ltresr  8206  addvalex  8211  axprecex  8247  elnnz  9654  fnn0ind  9762  rexuz2  9981  qreccl  10042  rexrp  10077  elixx3g  10303  elfz2  10418  elfzuzb  10422  fznn  10496  elfz2nn0  10519  fznn0  10520  4fvwrd4  10547  elfzo2  10557  fzind2  10658  sseqn  11279  hashf1lem1  11285  hashf1lem2  11286  cvg1nlemres  11751  fsum2dlemstep  12201  modfsummod  12225  fprodseq  12350  divalgb  12692  bezoutlemmain  12775  isprm2  12895  oddpwdc  12952  ballotfilemelo  13222  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  xpscf  13668  issubg3  13995  releqgg  14023  eqgex  14024  imasabl  14140  prdsex  14172  prdsval  14173  prdsbaslemss  14174  dfrhm2  14461  drngprop  14617  isassa  15002  ntreq0  15233  cnnei  15333  txlm  15380  blres  15535  isms2  15555  dedekindicclemicc  15733  limcrcl  15759  lgsquadlem1  16196  lgsquadlem2  16197  isclwwlknx  16657  clwwlknonel  16673  clwwlknon2x  16676  iseupthf1o  16689  bdcriota  16909  bj-peano4  16981  alsanmo  17151  ralsanmo  17152  alsralrex  17153  alsraln0m  17154