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  963  xorbi1d  1392  drsb1  1813  ax11ev  1842  eleq1w  2257  eleq1  2259  rexeqf  2690  reueq1f  2691  rmoeq1f  2692  rabeqf  2753  vtocl2gaf  2831  alexeq  2890  ceqex  2891  elrabi  2917  sbc5  3013  rexss  3251  ineq1  3358  difin2  3426  r19.28m  3541  preq12bg  3804  opeq1  3809  eluni  3843  disjiun  4029  mpteq12f  4114  axsep2  4153  zfauscl  4154  opthg  4272  copsexg  4278  euotd  4288  elopab  4293  pocl  4339  uniuni  4487  rabxfrd  4505  ontr2exmid  4562  regexmidlemm  4569  regexmidlem1  4570  reg2exmidlema  4571  preleq  4592  xpeq1  4678  elxpi  4680  vtoclr  4712  opbrop  4743  opelresg  4954  resopab2  4994  elxp4  5158  elxp5  5159  cnvpom  5213  fun11  5326  feq2  5394  f1eq2  5462  f1eq3  5463  foeq2  5480  brprcneu  5554  ssimaexg  5626  dmfco  5632  fndmdif  5670  rexsupp  5689  respreima  5693  isoeq5  5855  isoini  5868  isopolem  5872  f1oiso  5876  f1oiso2  5877  riotaeqdv  5881  acexmidlemab  5919  acexmidlemcase  5920  oprabid  5957  mpoeq123  5985  mpoeq123dva  5987  eloprabga  6013  resoprab  6022  resoprab2  6023  ov  6046  ovi3  6064  ov6g  6065  ovg  6066  caoftrn  6172  opabex3d  6187  opabex3  6188  elxp7  6237  eloprabi  6263  cnvf1o  6292  xporderlem  6298  poxp  6299  smoel2  6370  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  nnaordex  6595  qliftel  6683  brecop  6693  eroveu  6694  ecopovtrn  6700  ecopovtrng  6703  th3qlem2  6706  th3q  6708  ixpsnf1o  6804  dom2lem  6840  xpsnen  6889  xpassen  6898  pw2f1odclem  6904  xpf1o  6914  opabfi  7008  ctssdccl  7186  exmidapne  7343  dfplpq2  7438  dfmpq2  7439  ltsonq  7482  enq0sym  7516  enq0ref  7517  enq0tr  7518  enq0breq  7520  addnq0mo  7531  mulnq0mo  7532  addnnnq0  7533  mulnnnq0  7534  elinp  7558  prnmaxl  7572  prnminu  7573  prarloclemlo  7578  prarloc  7587  genpdflem  7591  genpassl  7608  genpassu  7609  ltexprlemm  7684  recexprlemell  7706  recexprlemelu  7707  cauappcvgprlemdisj  7735  caucvgprlemnkj  7750  caucvgprprlemnkltj  7773  caucvgprprlemnkeqj  7774  addsrmo  7827  mulsrmo  7828  addsrpr  7829  mulsrpr  7830  lttrsr  7846  mulgt0sr  7862  ltresr  7923  axpre-lttrn  7968  axpre-mulgt0  7971  recexgt0  8624  apreap  8631  apreim  8647  aprcl  8690  aptap  8694  prime  9442  rexuz  9671  ltxr  9867  ixxval  9988  fzval  10102  eqwrd  10992  sqrtrval  11182  abslt  11270  absle  11271  lenegsq  11277  abs2difabs  11290  2clim  11483  climcn2  11491  addcn2  11492  mulcn2  11494  climrecvg1n  11530  sumeq1  11537  fsum2dlemstep  11616  modfsummod  11640  prodeq1f  11734  fprod2dlemstep  11804  nndivdvds  11978  divalg2  12108  gcdval  12151  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlemex  12193  gcdass  12207  lcmval  12256  lcmass  12278  rpexp  12346  pythagtriplem2  12460  pythagtrip  12477  gsumfzval  13093  issgrpv  13106  issgrpn0  13107  ismhm  13163  mhmpropd  13168  issubm  13174  issubg  13379  issubg3  13398  ringpropd  13670  crngpropd  13671  opprunitd  13742  issubrg  13853  resrhm2b  13881  islmod  13923  lmodlema  13924  lmodprop2d  13980  islssm  13989  islssmg  13990  lsslss  14013  znleval  14285  psrbag  14299  istopg  14319  basis2  14368  tg2  14380  iscld  14423  neival  14463  isnei  14464  isneip  14466  iscn  14517  cnpval  14518  iscnp  14519  txbas  14578  txdis1cn  14598  ispsmet  14643  ismet  14664  isxmet  14665  ismet2  14674  blres  14754  elmopn  14766  mopni  14802  neibl  14811  metrest  14826  elcncf  14893  mulc1cncf  14909  mulcncf  14928  limccnp2lem  14996  sincosq2sgn  15147  sincosq4sgn  15149  2lgslem1a  15413  bdsep2  15616  bdzfauscl  15620  bj-d0clsepcl  15655  sscoll2  15718