Theorem anbi1d 465

Description: Deduction adding 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
anbid.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
anbi1d	|- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )

Proof of Theorem anbi1d

Step	Hyp	Ref	Expression
1		anbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	a1d 22	. 2 |- ( ph -> ( th -> ( ps <-> ch ) ) )
3	2	pm5.32rd 451	1 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ 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:  anbi1  466  anbi12d  473  bi2anan9  606  pm5.71dc  961  xorbi1d  1381  drsb1  1799  ax11ev  1828  eleq1w  2238  eleq1  2240  rexeqf  2669  reueq1f  2670  rmoeq1f  2671  rabeqf  2727  vtocl2gaf  2804  alexeq  2863  ceqex  2864  elrabi  2890  sbc5  2986  rexss  3222  ineq1  3329  difin2  3397  r19.28m  3512  preq12bg  3773  opeq1  3778  eluni  3812  disjiun  3998  mpteq12f  4083  axsep2  4122  zfauscl  4123  opthg  4238  copsexg  4244  euotd  4254  elopab  4258  pocl  4303  uniuni  4451  rabxfrd  4469  ontr2exmid  4524  regexmidlemm  4531  regexmidlem1  4532  reg2exmidlema  4533  preleq  4554  xpeq1  4640  elxpi  4642  vtoclr  4674  opbrop  4705  opelresg  4914  resopab2  4954  elxp4  5116  elxp5  5117  cnvpom  5171  fun11  5283  feq2  5349  f1eq2  5417  f1eq3  5418  foeq2  5435  brprcneu  5508  ssimaexg  5578  dmfco  5584  fndmdif  5621  rexsupp  5640  respreima  5644  isoeq5  5805  isoini  5818  isopolem  5822  f1oiso  5826  f1oiso2  5827  riotaeqdv  5831  acexmidlemab  5868  acexmidlemcase  5869  oprabid  5906  mpoeq123  5933  mpoeq123dva  5935  eloprabga  5961  resoprab  5970  resoprab2  5971  ov  5993  ovi3  6010  ov6g  6011  ovg  6012  caoftrn  6107  opabex3d  6121  opabex3  6122  elxp7  6170  eloprabi  6196  cnvf1o  6225  xporderlem  6231  poxp  6232  smoel2  6303  frec0g  6397  freccllem  6402  frecfcllem  6404  frecsuclem  6406  frecsuc  6407  nnaordex  6528  qliftel  6614  brecop  6624  eroveu  6625  ecopovtrn  6631  ecopovtrng  6634  th3qlem2  6637  th3q  6639  ixpsnf1o  6735  dom2lem  6771  xpsnen  6820  xpassen  6829  xpf1o  6843  ctssdccl  7109  exmidapne  7258  dfplpq2  7352  dfmpq2  7353  ltsonq  7396  enq0sym  7430  enq0ref  7431  enq0tr  7432  enq0breq  7434  addnq0mo  7445  mulnq0mo  7446  addnnnq0  7447  mulnnnq0  7448  elinp  7472  prnmaxl  7486  prnminu  7487  prarloclemlo  7492  prarloc  7501  genpdflem  7505  genpassl  7522  genpassu  7523  ltexprlemm  7598  recexprlemell  7620  recexprlemelu  7621  cauappcvgprlemdisj  7649  caucvgprlemnkj  7664  caucvgprprlemnkltj  7687  caucvgprprlemnkeqj  7688  addsrmo  7741  mulsrmo  7742  addsrpr  7743  mulsrpr  7744  lttrsr  7760  mulgt0sr  7776  ltresr  7837  axpre-lttrn  7882  axpre-mulgt0  7885  recexgt0  8536  apreap  8543  apreim  8559  aprcl  8602  aptap  8606  prime  9351  rexuz  9579  ltxr  9774  ixxval  9895  fzval  10009  sqrtrval  11008  abslt  11096  absle  11097  lenegsq  11103  abs2difabs  11116  2clim  11308  climcn2  11316  addcn2  11317  mulcn2  11319  climrecvg1n  11355  sumeq1  11362  fsum2dlemstep  11441  modfsummod  11465  prodeq1f  11559  fprod2dlemstep  11629  nndivdvds  11802  divalg2  11930  gcdval  11959  bezoutlemstep  11997  bezoutlemmain  11998  bezoutlemex  12001  gcdass  12015  lcmval  12062  lcmass  12084  rpexp  12152  pythagtriplem2  12265  pythagtrip  12282  issgrpv  12809  issgrpn0  12810  ismhm  12852  mhmpropd  12856  issubm  12862  issubg  13031  issubg3  13050  ringpropd  13215  crngpropd  13216  opprunitd  13277  issubrg  13340  islmod  13379  lmodlema  13380  istopg  13469  basis2  13518  tg2  13530  iscld  13573  neival  13613  isnei  13614  isneip  13616  iscn  13667  cnpval  13668  iscnp  13669  txbas  13728  txdis1cn  13748  ispsmet  13793  ismet  13814  isxmet  13815  ismet2  13824  blres  13904  elmopn  13916  mopni  13952  neibl  13961  metrest  13976  elcncf  14030  mulc1cncf  14046  mulcncf  14061  limccnp2lem  14115  sincosq2sgn  14218  sincosq4sgn  14220  bdsep2  14608  bdzfauscl  14612  bj-d0clsepcl  14647  sscoll2  14710