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  803  pm5.75  964  3ancoma  987  3ioran  995  an6  1332  19.26-3an  1497  19.28h  1576  19.28  1577  eeeanv  1952  sb3an  1977  moanim  2119  nfrexdya  2533  r19.26-3  2627  r19.41  2652  rexcomf  2659  3reeanv  2668  cbvreu  2727  ceqsex3v  2806  rexab  2926  rexrab  2927  rmo4  2957  rmo3f  2961  reuind  2969  sbc3an  3051  rmo3  3081  ssrab  3262  rexun  3344  elin3  3355  inass  3374  unssdif  3399  indifdir  3420  difin2  3426  inrab2  3437  rabun2  3443  reuun2  3447  undif4  3514  rexdifpr  3651  rexsns  3662  rexdifsn  3755  2ralunsn  3829  iuncom4  3924  iunxiun  3999  inuni  4189  unidif0  4201  bnd2  4207  otth2  4275  copsexg  4278  copsex4g  4281  opeqsn  4286  opelopabsbALT  4294  elpwpwel  4511  suc11g  4594  rabxp  4701  opeliunxp  4719  xpundir  4721  xpiundi  4722  xpiundir  4723  brinxp2  4731  rexiunxp  4809  brres  4953  brresg  4955  dmres  4968  resiexg  4992  dminss  5085  imainss  5086  ssrnres  5113  elxp4  5158  elxp5  5159  cnvresima  5160  coundi  5172  resco  5175  imaco  5176  coiun  5180  coi1  5186  coass  5189  xpcom  5217  dffun2  5269  fncnv  5325  imadiflem  5338  imadif  5339  imainlem  5340  mptun  5392  fcnvres  5444  dff1o2  5512  dff1o3  5513  ffoss  5539  f11o  5540  brprcneu  5554  fvun2  5631  eqfnfv3  5664  respreima  5693  f1ompt  5716  fsn  5737  abrexco  5809  imaiun  5810  f1mpt  5821  dff1o6  5826  oprabid  5957  dfoprab2  5973  oprab4  5997  mpomptx  6017  opabex3d  6187  opabex3  6188  abexssex  6191  dfopab2  6256  dfoprab3s  6257  1stconst  6288  2ndconst  6289  xporderlem  6298  spc2ed  6300  f1od2  6302  brtpos2  6318  tpostpos  6331  tposmpo  6348  oviec  6709  mapsncnv  6763  dfixp  6768  domen  6819  mapsnen  6879  xpsnen  6889  xpcomco  6894  xpassen  6898  ltexpi  7421  dfmq0qs  7513  dfplq0qs  7514  enq0enq  7515  enq0ref  7517  enq0tr  7518  nqnq0pi  7522  prnmaxl  7572  prnminu  7573  suplocexprlemloc  7805  addsrpr  7829  mulsrpr  7830  suplocsrlemb  7890  addcnsr  7918  mulcnsr  7919  ltresr  7923  addvalex  7928  axprecex  7964  elnnz  9353  fnn0ind  9459  rexuz2  9672  qreccl  9733  rexrp  9768  elixx3g  9993  elfz2  10107  elfzuzb  10111  fznn  10181  elfz2nn0  10204  fznn0  10205  4fvwrd4  10232  elfzo2  10242  fzind2  10332  cvg1nlemres  11167  fsum2dlemstep  11616  modfsummod  11640  fprodseq  11765  divalgb  12107  bezoutlemmain  12190  isprm2  12310  oddpwdc  12367  prdsex  12971  prdsval  12975  prdsbaslemss  12976  xpscf  13049  issubg3  13398  releqgg  13426  eqgex  13427  imasabl  13542  dfrhm2  13786  ntreq0  14452  cnnei  14552  txlm  14599  blres  14754  isms2  14774  dedekindicclemicc  14952  limcrcl  14978  lgsquadlem1  15402  lgsquadlem2  15403  bdcriota  15613  bj-peano4  15685  alsconv  15811