Theorem anbi1d 461

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi1  462  anbi12d  465  bi2anan9  596  pm5.71dc  946  xorbi1d  1360  drsb1  1776  ax11ev  1805  eleq1w  2215  eleq1  2217  rexeqf  2646  reueq1f  2647  rmoeq1f  2648  rabeqf  2699  vtocl2gaf  2776  alexeq  2835  ceqex  2836  elrabi  2861  sbc5  2956  rexss  3191  ineq1  3297  difin2  3365  r19.28m  3479  preq12bg  3732  opeq1  3737  eluni  3771  disjiun  3956  mpteq12f  4040  axsep2  4079  zfauscl  4080  opthg  4193  copsexg  4199  euotd  4209  elopab  4213  pocl  4258  uniuni  4405  rabxfrd  4423  ontr2exmid  4478  regexmidlemm  4485  regexmidlem1  4486  reg2exmidlema  4487  preleq  4508  xpeq1  4593  elxpi  4595  vtoclr  4627  opbrop  4658  opelresg  4866  resopab2  4906  elxp4  5066  elxp5  5067  cnvpom  5121  fun11  5230  feq2  5296  f1eq2  5364  f1eq3  5365  foeq2  5382  brprcneu  5454  ssimaexg  5523  dmfco  5529  fndmdif  5565  rexsupp  5584  respreima  5588  isoeq5  5746  isoini  5759  isopolem  5763  f1oiso  5767  f1oiso2  5768  riotaeqdv  5771  acexmidlemab  5808  acexmidlemcase  5809  oprabid  5843  mpoeq123  5870  mpoeq123dva  5872  eloprabga  5898  resoprab  5907  resoprab2  5908  ov  5930  ovi3  5947  ov6g  5948  ovg  5949  caoftrn  6047  opabex3d  6059  opabex3  6060  elxp7  6108  eloprabi  6134  cnvf1o  6162  xporderlem  6168  poxp  6169  smoel2  6240  frec0g  6334  freccllem  6339  frecfcllem  6341  frecsuclem  6343  frecsuc  6344  nnaordex  6463  qliftel  6549  brecop  6559  eroveu  6560  ecopovtrn  6566  ecopovtrng  6569  th3qlem2  6572  th3q  6574  ixpsnf1o  6670  dom2lem  6706  xpsnen  6755  xpassen  6764  xpf1o  6778  ctssdccl  7041  dfplpq2  7253  dfmpq2  7254  ltsonq  7297  enq0sym  7331  enq0ref  7332  enq0tr  7333  enq0breq  7335  addnq0mo  7346  mulnq0mo  7347  addnnnq0  7348  mulnnnq0  7349  elinp  7373  prnmaxl  7387  prnminu  7388  prarloclemlo  7393  prarloc  7402  genpdflem  7406  genpassl  7423  genpassu  7424  ltexprlemm  7499  recexprlemell  7521  recexprlemelu  7522  cauappcvgprlemdisj  7550  caucvgprlemnkj  7565  caucvgprprlemnkltj  7588  caucvgprprlemnkeqj  7589  addsrmo  7642  mulsrmo  7643  addsrpr  7644  mulsrpr  7645  lttrsr  7661  mulgt0sr  7677  ltresr  7738  axpre-lttrn  7783  axpre-mulgt0  7786  recexgt0  8434  apreap  8441  apreim  8457  aprcl  8500  prime  9242  rexuz  9470  ltxr  9660  ixxval  9778  fzval  9892  sqrtrval  10877  abslt  10965  absle  10966  lenegsq  10972  abs2difabs  10985  2clim  11175  climcn2  11183  addcn2  11184  mulcn2  11186  climrecvg1n  11222  sumeq1  11229  fsum2dlemstep  11308  modfsummod  11332  prodeq1f  11426  fprod2dlemstep  11496  nndivdvds  11666  divalg2  11790  gcdval  11815  bezoutlemstep  11853  bezoutlemmain  11854  bezoutlemex  11857  gcdass  11871  lcmval  11912  lcmass  11934  rpexp  11999  istopg  12344  basis2  12393  tg2  12407  iscld  12450  neival  12490  isnei  12491  isneip  12493  iscn  12544  cnpval  12545  iscnp  12546  txbas  12605  txdis1cn  12625  ispsmet  12670  ismet  12691  isxmet  12692  ismet2  12701  blres  12781  elmopn  12793  mopni  12829  neibl  12838  metrest  12853  elcncf  12907  mulc1cncf  12923  mulcncf  12938  limccnp2lem  12992  sincosq2sgn  13095  sincosq4sgn  13097  bdsep2  13407  bdzfauscl  13411  bj-d0clsepcl  13446  sscoll2  13509