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  951  xorbi1d  1371  drsb1  1787  ax11ev  1816  eleq1w  2226  eleq1  2228  rexeqf  2657  reueq1f  2658  rmoeq1f  2659  rabeqf  2715  vtocl2gaf  2792  alexeq  2851  ceqex  2852  elrabi  2878  sbc5  2973  rexss  3208  ineq1  3315  difin2  3383  r19.28m  3497  preq12bg  3752  opeq1  3757  eluni  3791  disjiun  3976  mpteq12f  4061  axsep2  4100  zfauscl  4101  opthg  4215  copsexg  4221  euotd  4231  elopab  4235  pocl  4280  uniuni  4428  rabxfrd  4446  ontr2exmid  4501  regexmidlemm  4508  regexmidlem1  4509  reg2exmidlema  4510  preleq  4531  xpeq1  4617  elxpi  4619  vtoclr  4651  opbrop  4682  opelresg  4890  resopab2  4930  elxp4  5090  elxp5  5091  cnvpom  5145  fun11  5254  feq2  5320  f1eq2  5388  f1eq3  5389  foeq2  5406  brprcneu  5478  ssimaexg  5547  dmfco  5553  fndmdif  5589  rexsupp  5608  respreima  5612  isoeq5  5772  isoini  5785  isopolem  5789  f1oiso  5793  f1oiso2  5794  riotaeqdv  5798  acexmidlemab  5835  acexmidlemcase  5836  oprabid  5870  mpoeq123  5897  mpoeq123dva  5899  eloprabga  5925  resoprab  5934  resoprab2  5935  ov  5957  ovi3  5974  ov6g  5975  ovg  5976  caoftrn  6074  opabex3d  6086  opabex3  6087  elxp7  6135  eloprabi  6161  cnvf1o  6189  xporderlem  6195  poxp  6196  smoel2  6267  frec0g  6361  freccllem  6366  frecfcllem  6368  frecsuclem  6370  frecsuc  6371  nnaordex  6491  qliftel  6577  brecop  6587  eroveu  6588  ecopovtrn  6594  ecopovtrng  6597  th3qlem2  6600  th3q  6602  ixpsnf1o  6698  dom2lem  6734  xpsnen  6783  xpassen  6792  xpf1o  6806  ctssdccl  7072  dfplpq2  7291  dfmpq2  7292  ltsonq  7335  enq0sym  7369  enq0ref  7370  enq0tr  7371  enq0breq  7373  addnq0mo  7384  mulnq0mo  7385  addnnnq0  7386  mulnnnq0  7387  elinp  7411  prnmaxl  7425  prnminu  7426  prarloclemlo  7431  prarloc  7440  genpdflem  7444  genpassl  7461  genpassu  7462  ltexprlemm  7537  recexprlemell  7559  recexprlemelu  7560  cauappcvgprlemdisj  7588  caucvgprlemnkj  7603  caucvgprprlemnkltj  7626  caucvgprprlemnkeqj  7627  addsrmo  7680  mulsrmo  7681  addsrpr  7682  mulsrpr  7683  lttrsr  7699  mulgt0sr  7715  ltresr  7776  axpre-lttrn  7821  axpre-mulgt0  7824  recexgt0  8474  apreap  8481  apreim  8497  aprcl  8540  prime  9286  rexuz  9514  ltxr  9707  ixxval  9828  fzval  9942  sqrtrval  10938  abslt  11026  absle  11027  lenegsq  11033  abs2difabs  11046  2clim  11238  climcn2  11246  addcn2  11247  mulcn2  11249  climrecvg1n  11285  sumeq1  11292  fsum2dlemstep  11371  modfsummod  11395  prodeq1f  11489  fprod2dlemstep  11559  nndivdvds  11732  divalg2  11859  gcdval  11888  bezoutlemstep  11926  bezoutlemmain  11927  bezoutlemex  11930  gcdass  11944  lcmval  11991  lcmass  12013  rpexp  12081  pythagtriplem2  12194  pythagtrip  12211  istopg  12597  basis2  12646  tg2  12660  iscld  12703  neival  12743  isnei  12744  isneip  12746  iscn  12797  cnpval  12798  iscnp  12799  txbas  12858  txdis1cn  12878  ispsmet  12923  ismet  12944  isxmet  12945  ismet2  12954  blres  13034  elmopn  13046  mopni  13082  neibl  13091  metrest  13106  elcncf  13160  mulc1cncf  13176  mulcncf  13191  limccnp2lem  13245  sincosq2sgn  13348  sincosq4sgn  13350  bdsep2  13728  bdzfauscl  13732  bj-d0clsepcl  13767  sscoll2  13830