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  964  xorbi1d  1401  drsb1  1823  ax11ev  1852  eleq1w  2268  eleq1  2270  rexeqf  2702  reueq1f  2703  rmoeq1f  2704  rabeqf  2766  vtocl2gaf  2845  alexeq  2906  ceqex  2907  elrabi  2933  sbc5  3029  rexss  3268  ineq1  3375  difin2  3443  r19.28m  3558  elif  3591  preq12bg  3827  opeq1  3833  eluni  3867  disjiun  4054  mpteq12f  4140  axsep2  4179  zfauscl  4180  opthg  4300  copsexg  4306  euotd  4317  elopab  4322  pocl  4368  uniuni  4516  rabxfrd  4534  ontr2exmid  4591  regexmidlemm  4598  regexmidlem1  4599  reg2exmidlema  4600  preleq  4621  xpeq1  4707  elxpi  4709  vtoclr  4741  opbrop  4772  opelresg  4985  resopab2  5025  elxp4  5189  elxp5  5190  cnvpom  5244  fun11  5360  feq2  5429  f1eq2  5499  f1eq3  5500  foeq2  5517  brprcneu  5592  ssimaexg  5664  dmfco  5670  fndmdif  5708  rexsupp  5727  respreima  5731  isoeq5  5897  isoini  5910  isopolem  5914  f1oiso  5918  f1oiso2  5919  riotaeqdv  5923  acexmidlemab  5961  acexmidlemcase  5962  oprabid  5999  mpoeq123  6027  mpoeq123dva  6029  eloprabga  6055  resoprab  6064  resoprab2  6065  ov  6088  ovi3  6106  ov6g  6107  ovg  6108  caoftrn  6214  opabex3d  6229  opabex3  6230  elxp7  6279  eloprabi  6305  cnvf1o  6334  xporderlem  6340  poxp  6341  smoel2  6412  frec0g  6506  freccllem  6511  frecfcllem  6513  frecsuclem  6515  frecsuc  6516  nnaordex  6637  qliftel  6725  brecop  6735  eroveu  6736  ecopovtrn  6742  ecopovtrng  6745  th3qlem2  6748  th3q  6750  ixpsnf1o  6846  dom2lem  6886  xpsnen  6941  xpassen  6950  pw2f1odclem  6956  xpf1o  6966  opabfi  7061  ctssdccl  7239  exmidapne  7407  dfplpq2  7502  dfmpq2  7503  ltsonq  7546  enq0sym  7580  enq0ref  7581  enq0tr  7582  enq0breq  7584  addnq0mo  7595  mulnq0mo  7596  addnnnq0  7597  mulnnnq0  7598  elinp  7622  prnmaxl  7636  prnminu  7637  prarloclemlo  7642  prarloc  7651  genpdflem  7655  genpassl  7672  genpassu  7673  ltexprlemm  7748  recexprlemell  7770  recexprlemelu  7771  cauappcvgprlemdisj  7799  caucvgprlemnkj  7814  caucvgprprlemnkltj  7837  caucvgprprlemnkeqj  7838  addsrmo  7891  mulsrmo  7892  addsrpr  7893  mulsrpr  7894  lttrsr  7910  mulgt0sr  7926  ltresr  7987  axpre-lttrn  8032  axpre-mulgt0  8035  recexgt0  8688  apreap  8695  apreim  8711  aprcl  8754  aptap  8758  prime  9507  rexuz  9736  ltxr  9932  ixxval  10053  fzval  10167  eqwrd  11071  pfxeq  11187  wrd2ind  11214  sqrtrval  11426  abslt  11514  absle  11515  lenegsq  11521  abs2difabs  11534  2clim  11727  climcn2  11735  addcn2  11736  mulcn2  11738  climrecvg1n  11774  sumeq1  11781  fsum2dlemstep  11860  modfsummod  11884  prodeq1f  11978  fprod2dlemstep  12048  nndivdvds  12222  divalg2  12352  gcdval  12395  bezoutlemstep  12433  bezoutlemmain  12434  bezoutlemex  12437  gcdass  12451  lcmval  12500  lcmass  12522  rpexp  12590  pythagtriplem2  12704  pythagtrip  12721  gsumfzval  13338  issgrpv  13351  issgrpn0  13352  ismhm  13408  mhmpropd  13413  issubm  13419  issubg  13624  issubg3  13643  ringpropd  13915  crngpropd  13916  opprunitd  13987  issubrg  14098  resrhm2b  14126  islmod  14168  lmodlema  14169  lmodprop2d  14225  islssm  14234  islssmg  14235  lsslss  14258  znleval  14530  psrbag  14546  istopg  14586  basis2  14635  tg2  14647  iscld  14690  neival  14730  isnei  14731  isneip  14733  iscn  14784  cnpval  14785  iscnp  14786  txbas  14845  txdis1cn  14865  ispsmet  14910  ismet  14931  isxmet  14932  ismet2  14941  blres  15021  elmopn  15033  mopni  15069  neibl  15078  metrest  15093  elcncf  15160  mulc1cncf  15176  mulcncf  15195  limccnp2lem  15263  sincosq2sgn  15414  sincosq4sgn  15416  2lgslem1a  15680  bdsep2  16021  bdzfauscl  16025  bj-d0clsepcl  16060  sscoll2  16123