Theorem anbi1d 465

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anbi1  466  anbi12d  473  bi2anan9  606  pm5.71dc  963  xorbi1d  1392  drsb1  1810  ax11ev  1839  eleq1w  2254  eleq1  2256  rexeqf  2687  reueq1f  2688  rmoeq1f  2689  rabeqf  2750  vtocl2gaf  2828  alexeq  2887  ceqex  2888  elrabi  2914  sbc5  3010  rexss  3247  ineq1  3354  difin2  3422  r19.28m  3537  preq12bg  3800  opeq1  3805  eluni  3839  disjiun  4025  mpteq12f  4110  axsep2  4149  zfauscl  4150  opthg  4268  copsexg  4274  euotd  4284  elopab  4289  pocl  4335  uniuni  4483  rabxfrd  4501  ontr2exmid  4558  regexmidlemm  4565  regexmidlem1  4566  reg2exmidlema  4567  preleq  4588  xpeq1  4674  elxpi  4676  vtoclr  4708  opbrop  4739  opelresg  4950  resopab2  4990  elxp4  5154  elxp5  5155  cnvpom  5209  fun11  5322  feq2  5388  f1eq2  5456  f1eq3  5457  foeq2  5474  brprcneu  5548  ssimaexg  5620  dmfco  5626  fndmdif  5664  rexsupp  5683  respreima  5687  isoeq5  5849  isoini  5862  isopolem  5866  f1oiso  5870  f1oiso2  5871  riotaeqdv  5875  acexmidlemab  5913  acexmidlemcase  5914  oprabid  5951  mpoeq123  5978  mpoeq123dva  5980  eloprabga  6006  resoprab  6015  resoprab2  6016  ov  6039  ovi3  6057  ov6g  6058  ovg  6059  caoftrn  6160  opabex3d  6175  opabex3  6176  elxp7  6225  eloprabi  6251  cnvf1o  6280  xporderlem  6286  poxp  6287  smoel2  6358  frec0g  6452  freccllem  6457  frecfcllem  6459  frecsuclem  6461  frecsuc  6462  nnaordex  6583  qliftel  6671  brecop  6681  eroveu  6682  ecopovtrn  6688  ecopovtrng  6691  th3qlem2  6694  th3q  6696  ixpsnf1o  6792  dom2lem  6828  xpsnen  6877  xpassen  6886  pw2f1odclem  6892  xpf1o  6902  opabfi  6994  ctssdccl  7172  exmidapne  7322  dfplpq2  7416  dfmpq2  7417  ltsonq  7460  enq0sym  7494  enq0ref  7495  enq0tr  7496  enq0breq  7498  addnq0mo  7509  mulnq0mo  7510  addnnnq0  7511  mulnnnq0  7512  elinp  7536  prnmaxl  7550  prnminu  7551  prarloclemlo  7556  prarloc  7565  genpdflem  7569  genpassl  7586  genpassu  7587  ltexprlemm  7662  recexprlemell  7684  recexprlemelu  7685  cauappcvgprlemdisj  7713  caucvgprlemnkj  7728  caucvgprprlemnkltj  7751  caucvgprprlemnkeqj  7752  addsrmo  7805  mulsrmo  7806  addsrpr  7807  mulsrpr  7808  lttrsr  7824  mulgt0sr  7840  ltresr  7901  axpre-lttrn  7946  axpre-mulgt0  7949  recexgt0  8601  apreap  8608  apreim  8624  aprcl  8667  aptap  8671  prime  9419  rexuz  9648  ltxr  9844  ixxval  9965  fzval  10079  eqwrd  10957  sqrtrval  11147  abslt  11235  absle  11236  lenegsq  11242  abs2difabs  11255  2clim  11447  climcn2  11455  addcn2  11456  mulcn2  11458  climrecvg1n  11494  sumeq1  11501  fsum2dlemstep  11580  modfsummod  11604  prodeq1f  11698  fprod2dlemstep  11768  nndivdvds  11942  divalg2  12070  gcdval  12099  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlemex  12141  gcdass  12155  lcmval  12204  lcmass  12226  rpexp  12294  pythagtriplem2  12407  pythagtrip  12424  gsumfzval  12977  issgrpv  12990  issgrpn0  12991  ismhm  13036  mhmpropd  13041  issubm  13047  issubg  13246  issubg3  13265  ringpropd  13537  crngpropd  13538  opprunitd  13609  issubrg  13720  resrhm2b  13748  islmod  13790  lmodlema  13791  lmodprop2d  13847  islssm  13856  islssmg  13857  lsslss  13880  znleval  14152  psrbag  14166  istopg  14178  basis2  14227  tg2  14239  iscld  14282  neival  14322  isnei  14323  isneip  14325  iscn  14376  cnpval  14377  iscnp  14378  txbas  14437  txdis1cn  14457  ispsmet  14502  ismet  14523  isxmet  14524  ismet2  14533  blres  14613  elmopn  14625  mopni  14661  neibl  14670  metrest  14685  elcncf  14752  mulc1cncf  14768  mulcncf  14787  limccnp2lem  14855  sincosq2sgn  15003  sincosq4sgn  15005  2lgslem1a  15245  bdsep2  15448  bdzfauscl  15452  bj-d0clsepcl  15487  sscoll2  15550