Theorem anbi1d 452

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anbi1  453  anbi12d  456  bi2anan9  570  pm5.71dc  902  xorbi1d  1312  drsb1  1720  ax11ev  1749  eleq1  2141  rexeqf  2546  reueq1f  2547  rmoeq1f  2548  rabeqf  2594  vtocl2gaf  2665  alexeq  2721  ceqex  2722  elrabi  2746  sbc5  2838  rexss  3061  ineq1  3160  difin2  3226  r19.28m  3331  preq12bg  3565  opeq1  3570  eluni  3604  mpteq12f  3858  axsep2  3897  zfauscl  3898  opthg  3993  copsexg  3999  euotd  4009  elopab  4013  pocl  4058  uniuni  4201  rabxfrd  4219  ontr2exmid  4268  regexmidlemm  4275  regexmidlem1  4276  reg2exmidlema  4277  preleq  4298  xpeq1  4377  elxpi  4379  vtoclr  4406  opbrop  4437  opelresg  4637  resopab2  4675  elxp4  4828  elxp5  4829  cnvpom  4880  fun11  4986  feq2  5051  f1eq2  5108  f1eq3  5109  foeq2  5123  brprcneu  5191  ssimaexg  5256  dmfco  5262  fndmdif  5293  rexsupp  5312  respreima  5316  isoeq5  5465  isoini  5477  isopolem  5481  f1oiso  5485  f1oiso2  5486  riotaeqdv  5489  acexmidlemab  5526  acexmidlemcase  5527  oprabid  5557  mpt2eq123  5584  mpt2eq123dva  5586  eloprabga  5611  resoprab  5617  resoprab2  5618  ov  5640  ovi3  5657  ov6g  5658  ovg  5659  caoftrn  5756  opabex3d  5768  opabex3  5769  elxp7  5817  eloprabi  5842  cnvf1o  5866  xporderlem  5872  poxp  5873  smoel2  5941  frec0g  6006  frecsuclem3  6013  frecsuc  6014  nnaordex  6123  qliftel  6209  brecop  6219  eroveu  6220  ecopovtrn  6226  ecopovtrng  6229  th3qlem2  6232  th3q  6234  dom2lem  6275  xpsnen  6318  xpassen  6327  dfplpq2  6544  dfmpq2  6545  ltsonq  6588  enq0sym  6622  enq0ref  6623  enq0tr  6624  enq0breq  6626  addnq0mo  6637  mulnq0mo  6638  addnnnq0  6639  mulnnnq0  6640  elinp  6664  prnmaxl  6678  prnminu  6679  prarloclemlo  6684  prarloc  6693  genpdflem  6697  genpassl  6714  genpassu  6715  ltexprlemm  6790  recexprlemell  6812  recexprlemelu  6813  cauappcvgprlemdisj  6841  caucvgprlemnkj  6856  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  addsrmo  6920  mulsrmo  6921  addsrpr  6922  mulsrpr  6923  lttrsr  6939  mulgt0sr  6954  ltresr  7007  axpre-lttrn  7050  axpre-mulgt0  7053  recexgt0  7680  apreap  7687  apreim  7703  prime  8446  rexuz  8668  ltxr  8849  ixxval  8919  fzval  9031  sqrtrval  9886  abslt  9974  absle  9975  lenegsq  9981  abs2difabs  9994  2clim  10140  climcn2  10148  addcn2  10149  mulcn2  10151  climrecvg1n  10185  sumeq1  10192  nndivdvds  10201  divalg2  10326  gcdval  10351  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlemex  10390  gcdass  10404  lcmval  10445  lcmass  10467  rpexp  10532  bdsep2  10677  bdzfauscl  10681  bj-d0clsepcl  10720