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  1494  19.28h  1573  19.28  1574  eeeanv  1949  sb3an  1974  moanim  2116  nfrexdya  2530  r19.26-3  2624  r19.41  2649  rexcomf  2656  3reeanv  2665  cbvreu  2724  ceqsex3v  2802  rexab  2922  rexrab  2923  rmo4  2953  rmo3f  2957  reuind  2965  sbc3an  3047  rmo3  3077  ssrab  3257  rexun  3339  elin3  3350  inass  3369  unssdif  3394  indifdir  3415  difin2  3421  inrab2  3432  rabun2  3438  reuun2  3442  undif4  3509  rexdifpr  3646  rexsns  3657  rexdifsn  3750  2ralunsn  3824  iuncom4  3919  iunxiun  3994  inuni  4184  unidif0  4196  bnd2  4202  otth2  4270  copsexg  4273  copsex4g  4276  opeqsn  4281  opelopabsbALT  4289  elpwpwel  4506  suc11g  4589  rabxp  4696  opeliunxp  4714  xpundir  4716  xpiundi  4717  xpiundir  4718  brinxp2  4726  rexiunxp  4804  brres  4948  brresg  4950  dmres  4963  resiexg  4987  dminss  5080  imainss  5081  ssrnres  5108  elxp4  5153  elxp5  5154  cnvresima  5155  coundi  5167  resco  5170  imaco  5171  coiun  5175  coi1  5181  coass  5184  xpcom  5212  dffun2  5264  fncnv  5320  imadiflem  5333  imadif  5334  imainlem  5335  mptun  5385  fcnvres  5437  dff1o2  5505  dff1o3  5506  ffoss  5532  f11o  5533  brprcneu  5547  fvun2  5624  eqfnfv3  5657  respreima  5686  f1ompt  5709  fsn  5730  abrexco  5802  imaiun  5803  f1mpt  5814  dff1o6  5819  oprabid  5950  dfoprab2  5965  oprab4  5989  mpomptx  6009  opabex3d  6173  opabex3  6174  abexssex  6177  dfopab2  6242  dfoprab3s  6243  1stconst  6274  2ndconst  6275  xporderlem  6284  spc2ed  6286  f1od2  6288  brtpos2  6304  tpostpos  6317  tposmpo  6334  oviec  6695  mapsncnv  6749  dfixp  6754  domen  6805  mapsnen  6865  xpsnen  6875  xpcomco  6880  xpassen  6884  ltexpi  7397  dfmq0qs  7489  dfplq0qs  7490  enq0enq  7491  enq0ref  7493  enq0tr  7494  nqnq0pi  7498  prnmaxl  7548  prnminu  7549  suplocexprlemloc  7781  addsrpr  7805  mulsrpr  7806  suplocsrlemb  7866  addcnsr  7894  mulcnsr  7895  ltresr  7899  addvalex  7904  axprecex  7940  elnnz  9327  fnn0ind  9433  rexuz2  9646  qreccl  9707  rexrp  9742  elixx3g  9967  elfz2  10081  elfzuzb  10085  fznn  10155  elfz2nn0  10178  fznn0  10179  4fvwrd4  10206  elfzo2  10216  fzind2  10306  cvg1nlemres  11129  fsum2dlemstep  11577  modfsummod  11601  fprodseq  11726  divalgb  12066  bezoutlemmain  12135  isprm2  12255  oddpwdc  12312  prdsex  12880  xpscf  12930  issubg3  13262  releqgg  13290  eqgex  13291  imasabl  13406  dfrhm2  13650  ntreq0  14300  cnnei  14400  txlm  14447  blres  14602  isms2  14622  dedekindicclemicc  14786  limcrcl  14812  lgsquadlem1  15191  bdcriota  15375  bj-peano4  15447  alsconv  15570