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  9658  fnn0ind  9766  rexuz2  9990  qreccl  10051  rexrp  10087  elixx3g  10313  elfz2  10428  elfzuzb  10432  fznn  10506  elfz2nn0  10529  fznn0  10530  4fvwrd4  10557  elfzo2  10567  fzind2  10668  sseqn  11293  hashf1lem1  11299  hashf1lem2  11300  cvg1nlemres  11765  fsum2dlemstep  12217  modfsummod  12241  fprodseq  12366  divalgb  12708  bezoutlemmain  12791  isprm2  12911  nnmaxpw  12969  ballotfilemelo  13271  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  xpscf  13717  issubg3  14044  releqgg  14072  eqgex  14073  imasabl  14189  prdsex  14221  prdsval  14222  prdsbaslemss  14223  dfrhm2  14510  drngprop  14666  isassa  15051  ntreq0  15282  cnnei  15382  txlm  15429  blres  15584  isms2  15604  dedekindicclemicc  15782  limcrcl  15808  lgsquadlem1  16294  lgsquadlem2  16295  isclwwlknx  16755  clwwlknonel  16771  clwwlknon2x  16774  iseupthf1o  16787  bdcriota  17007  bj-peano4  17079  alsanmo  17249  ralsanmo  17250  alsralrex  17251  alsraln0m  17252