Theorem anbi1i 431

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

Syntax hints:   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  anbi2ci  432  anbi12i  433  an12  495  anandi  524  pm5.53  714  pm5.75  868  3ancoma  891  3ioran  899  an6  1215  19.26-3an  1369  19.28h  1451  19.28  1452  eeeanv  1805  sb3an  1829  moanim  1971  nfrexdya  2353  r19.26-3  2437  r19.41  2459  rexcomf  2466  3reeanv  2474  cbvreu  2525  ceqsex3v  2590  rexab  2697  rexrab  2698  rmo4  2728  reuind  2738  rmo3  2843  ssrab  3012  rexun  3117  elin3  3122  inass  3141  unssdif  3166  indifdir  3187  difin2  3193  inrab2  3204  rabun2  3210  reuun2  3214  undif4  3278  rexsns  3400  rexsnsOLD  3401  rexdifsn  3490  2ralunsn  3560  iuncom4  3655  iunxiun  3727  inuni  3900  unidif0  3911  bnd2  3917  otth2  3969  copsexg  3972  copsex4g  3975  opeqsn  3980  opelopabsbALT  3987  suc11g  4235  rabxp  4323  opeliunxp  4338  xpundir  4340  xpiundi  4341  xpiundir  4342  brinxp2  4350  rexiunxp  4421  brres  4561  brresg  4563  dmres  4575  resiexg  4596  dminss  4681  imainss  4682  ssrnres  4706  elxp4  4751  elxp5  4752  cnvresima  4753  coundi  4765  resco  4768  imaco  4769  coiun  4773  coi1  4779  coass  4782  xpcom  4807  dffun2  4855  fncnv  4908  imadiflem  4921  imadif  4922  imainlem  4923  mptun  4972  fcnvres  5016  dff1o2  5074  dff1o3  5075  ffoss  5101  f11o  5102  brprcneu  5114  fvun2  5183  eqfnfv3  5210  respreima  5238  f1ompt  5263  fsn  5278  abrexco  5341  imaiun  5342  f1mpt  5353  dff1o6  5359  oprabid  5480  dfoprab2  5494  oprab4  5517  mpt2mptx  5537  opabex3d  5690  opabex3  5691  abexssex  5694  dfopab2  5757  dfoprab3s  5758  1stconst  5784  2ndconst  5785  xporderlem  5793  brtpos2  5807  tpostpos  5820  tposmpt2  5837  oviec  6148  domen  6168  xpsnen  6231  xpcomco  6236  xpassen  6240  ltexpi  6321  dfmq0qs  6411  dfplq0qs  6412  enq0enq  6413  enq0ref  6415  enq0tr  6416  nqnq0pi  6420  prnmaxl  6470  prnminu  6471  addsrpr  6633  mulsrpr  6634  addcnsr  6691  mulcnsr  6692  ltresr  6696  axprecex  6724  elnnz  7991  fnn0ind  8090  rexuz2  8260  qreccl  8311  rexrp  8340  elixx3g  8500  elfz2  8611  elfzuzb  8614  fznn  8681  elfz2nn0  8703  fznn0  8704  4fvwrd4  8727  elfzo2  8737  fzind2  8825  bdcriota  9272  bj-peano4  9343  alsconv  9377