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  1772  ax11ev  1801  eleq1w  2201  eleq1  2203  rexeqf  2626  reueq1f  2627  rmoeq1f  2628  rabeqf  2679  vtocl2gaf  2756  alexeq  2815  ceqex  2816  elrabi  2841  sbc5  2936  rexss  3169  ineq1  3275  difin2  3343  r19.28m  3457  preq12bg  3708  opeq1  3713  eluni  3747  disjiun  3932  mpteq12f  4016  axsep2  4055  zfauscl  4056  opthg  4168  copsexg  4174  euotd  4184  elopab  4188  pocl  4233  uniuni  4380  rabxfrd  4398  ontr2exmid  4448  regexmidlemm  4455  regexmidlem1  4456  reg2exmidlema  4457  preleq  4478  xpeq1  4561  elxpi  4563  vtoclr  4595  opbrop  4626  opelresg  4834  resopab2  4874  elxp4  5034  elxp5  5035  cnvpom  5089  fun11  5198  feq2  5264  f1eq2  5332  f1eq3  5333  foeq2  5350  brprcneu  5422  ssimaexg  5491  dmfco  5497  fndmdif  5533  rexsupp  5552  respreima  5556  isoeq5  5714  isoini  5727  isopolem  5731  f1oiso  5735  f1oiso2  5736  riotaeqdv  5739  acexmidlemab  5776  acexmidlemcase  5777  oprabid  5811  mpoeq123  5838  mpoeq123dva  5840  eloprabga  5866  resoprab  5875  resoprab2  5876  ov  5898  ovi3  5915  ov6g  5916  ovg  5917  caoftrn  6015  opabex3d  6027  opabex3  6028  elxp7  6076  eloprabi  6102  cnvf1o  6130  xporderlem  6136  poxp  6137  smoel2  6208  frec0g  6302  freccllem  6307  frecfcllem  6309  frecsuclem  6311  frecsuc  6312  nnaordex  6431  qliftel  6517  brecop  6527  eroveu  6528  ecopovtrn  6534  ecopovtrng  6537  th3qlem2  6540  th3q  6542  ixpsnf1o  6638  dom2lem  6674  xpsnen  6723  xpassen  6732  xpf1o  6746  ctssdccl  7004  dfplpq2  7186  dfmpq2  7187  ltsonq  7230  enq0sym  7264  enq0ref  7265  enq0tr  7266  enq0breq  7268  addnq0mo  7279  mulnq0mo  7280  addnnnq0  7281  mulnnnq0  7282  elinp  7306  prnmaxl  7320  prnminu  7321  prarloclemlo  7326  prarloc  7335  genpdflem  7339  genpassl  7356  genpassu  7357  ltexprlemm  7432  recexprlemell  7454  recexprlemelu  7455  cauappcvgprlemdisj  7483  caucvgprlemnkj  7498  caucvgprprlemnkltj  7521  caucvgprprlemnkeqj  7522  addsrmo  7575  mulsrmo  7576  addsrpr  7577  mulsrpr  7578  lttrsr  7594  mulgt0sr  7610  ltresr  7671  axpre-lttrn  7716  axpre-mulgt0  7719  recexgt0  8366  apreap  8373  apreim  8389  aprcl  8432  prime  9174  rexuz  9402  ltxr  9592  ixxval  9709  fzval  9823  sqrtrval  10804  abslt  10892  absle  10893  lenegsq  10899  abs2difabs  10912  2clim  11102  climcn2  11110  addcn2  11111  mulcn2  11113  climrecvg1n  11149  sumeq1  11156  fsum2dlemstep  11235  modfsummod  11259  prodeq1f  11353  nndivdvds  11535  divalg2  11659  gcdval  11684  bezoutlemstep  11721  bezoutlemmain  11722  bezoutlemex  11725  gcdass  11739  lcmval  11780  lcmass  11802  rpexp  11867  istopg  12205  basis2  12254  tg2  12268  iscld  12311  neival  12351  isnei  12352  isneip  12354  iscn  12405  cnpval  12406  iscnp  12407  txbas  12466  txdis1cn  12486  ispsmet  12531  ismet  12552  isxmet  12553  ismet2  12562  blres  12642  elmopn  12654  mopni  12690  neibl  12699  metrest  12714  elcncf  12768  mulc1cncf  12784  mulcncf  12799  limccnp2lem  12853  sincosq2sgn  12956  sincosq4sgn  12958  bdsep2  13255  bdzfauscl  13259  bj-d0clsepcl  13294  sscoll2  13357