Theorem anbi1d 460

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 446	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  461  anbi12d  464  bi2anan9  595  pm5.71dc  945  xorbi1d  1359  drsb1  1771  ax11ev  1800  eleq1w  2200  eleq1  2202  rexeqf  2623  reueq1f  2624  rmoeq1f  2625  rabeqf  2676  vtocl2gaf  2753  alexeq  2811  ceqex  2812  elrabi  2837  sbc5  2932  rexss  3164  ineq1  3270  difin2  3338  r19.28m  3452  preq12bg  3700  opeq1  3705  eluni  3739  disjiun  3924  mpteq12f  4008  axsep2  4047  zfauscl  4048  opthg  4160  copsexg  4166  euotd  4176  elopab  4180  pocl  4225  uniuni  4372  rabxfrd  4390  ontr2exmid  4440  regexmidlemm  4447  regexmidlem1  4448  reg2exmidlema  4449  preleq  4470  xpeq1  4553  elxpi  4555  vtoclr  4587  opbrop  4618  opelresg  4826  resopab2  4866  elxp4  5026  elxp5  5027  cnvpom  5081  fun11  5190  feq2  5256  f1eq2  5324  f1eq3  5325  foeq2  5342  brprcneu  5414  ssimaexg  5483  dmfco  5489  fndmdif  5525  rexsupp  5544  respreima  5548  isoeq5  5706  isoini  5719  isopolem  5723  f1oiso  5727  f1oiso2  5728  riotaeqdv  5731  acexmidlemab  5768  acexmidlemcase  5769  oprabid  5803  mpoeq123  5830  mpoeq123dva  5832  eloprabga  5858  resoprab  5867  resoprab2  5868  ov  5890  ovi3  5907  ov6g  5908  ovg  5909  caoftrn  6007  opabex3d  6019  opabex3  6020  elxp7  6068  eloprabi  6094  cnvf1o  6122  xporderlem  6128  poxp  6129  smoel2  6200  frec0g  6294  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecsuc  6304  nnaordex  6423  qliftel  6509  brecop  6519  eroveu  6520  ecopovtrn  6526  ecopovtrng  6529  th3qlem2  6532  th3q  6534  ixpsnf1o  6630  dom2lem  6666  xpsnen  6715  xpassen  6724  xpf1o  6738  ctssdccl  6996  dfplpq2  7162  dfmpq2  7163  ltsonq  7206  enq0sym  7240  enq0ref  7241  enq0tr  7242  enq0breq  7244  addnq0mo  7255  mulnq0mo  7256  addnnnq0  7257  mulnnnq0  7258  elinp  7282  prnmaxl  7296  prnminu  7297  prarloclemlo  7302  prarloc  7311  genpdflem  7315  genpassl  7332  genpassu  7333  ltexprlemm  7408  recexprlemell  7430  recexprlemelu  7431  cauappcvgprlemdisj  7459  caucvgprlemnkj  7474  caucvgprprlemnkltj  7497  caucvgprprlemnkeqj  7498  addsrmo  7551  mulsrmo  7552  addsrpr  7553  mulsrpr  7554  lttrsr  7570  mulgt0sr  7586  ltresr  7647  axpre-lttrn  7692  axpre-mulgt0  7695  recexgt0  8342  apreap  8349  apreim  8365  aprcl  8408  prime  9150  rexuz  9375  ltxr  9562  ixxval  9679  fzval  9792  sqrtrval  10772  abslt  10860  absle  10861  lenegsq  10867  abs2difabs  10880  2clim  11070  climcn2  11078  addcn2  11079  mulcn2  11081  climrecvg1n  11117  sumeq1  11124  fsum2dlemstep  11203  modfsummod  11227  prodeq1f  11321  nndivdvds  11499  divalg2  11623  gcdval  11648  bezoutlemstep  11685  bezoutlemmain  11686  bezoutlemex  11689  gcdass  11703  lcmval  11744  lcmass  11766  rpexp  11831  istopg  12166  basis2  12215  tg2  12229  iscld  12272  neival  12312  isnei  12313  isneip  12315  iscn  12366  cnpval  12367  iscnp  12368  txbas  12427  txdis1cn  12447  ispsmet  12492  ismet  12513  isxmet  12514  ismet2  12523  blres  12603  elmopn  12615  mopni  12651  neibl  12660  metrest  12675  elcncf  12729  mulc1cncf  12745  mulcncf  12760  limccnp2lem  12814  sincosq2sgn  12908  sincosq4sgn  12910  bdsep2  13084  bdzfauscl  13088  bj-d0clsepcl  13123