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  2827  alexeq  2886  ceqex  2887  elrabi  2913  sbc5  3009  rexss  3246  ineq1  3353  difin2  3421  r19.28m  3536  preq12bg  3799  opeq1  3804  eluni  3838  disjiun  4024  mpteq12f  4109  axsep2  4148  zfauscl  4149  opthg  4267  copsexg  4273  euotd  4283  elopab  4288  pocl  4334  uniuni  4482  rabxfrd  4500  ontr2exmid  4557  regexmidlemm  4564  regexmidlem1  4565  reg2exmidlema  4566  preleq  4587  xpeq1  4673  elxpi  4675  vtoclr  4707  opbrop  4738  opelresg  4949  resopab2  4989  elxp4  5153  elxp5  5154  cnvpom  5208  fun11  5321  feq2  5387  f1eq2  5455  f1eq3  5456  foeq2  5473  brprcneu  5547  ssimaexg  5619  dmfco  5625  fndmdif  5663  rexsupp  5682  respreima  5686  isoeq5  5848  isoini  5861  isopolem  5865  f1oiso  5869  f1oiso2  5870  riotaeqdv  5874  acexmidlemab  5912  acexmidlemcase  5913  oprabid  5950  mpoeq123  5977  mpoeq123dva  5979  eloprabga  6005  resoprab  6014  resoprab2  6015  ov  6038  ovi3  6055  ov6g  6056  ovg  6057  caoftrn  6158  opabex3d  6173  opabex3  6174  elxp7  6223  eloprabi  6249  cnvf1o  6278  xporderlem  6284  poxp  6285  smoel2  6356  frec0g  6450  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecsuc  6460  nnaordex  6581  qliftel  6669  brecop  6679  eroveu  6680  ecopovtrn  6686  ecopovtrng  6689  th3qlem2  6692  th3q  6694  ixpsnf1o  6790  dom2lem  6826  xpsnen  6875  xpassen  6884  pw2f1odclem  6890  xpf1o  6900  opabfi  6992  ctssdccl  7170  exmidapne  7320  dfplpq2  7414  dfmpq2  7415  ltsonq  7458  enq0sym  7492  enq0ref  7493  enq0tr  7494  enq0breq  7496  addnq0mo  7507  mulnq0mo  7508  addnnnq0  7509  mulnnnq0  7510  elinp  7534  prnmaxl  7548  prnminu  7549  prarloclemlo  7554  prarloc  7563  genpdflem  7567  genpassl  7584  genpassu  7585  ltexprlemm  7660  recexprlemell  7682  recexprlemelu  7683  cauappcvgprlemdisj  7711  caucvgprlemnkj  7726  caucvgprprlemnkltj  7749  caucvgprprlemnkeqj  7750  addsrmo  7803  mulsrmo  7804  addsrpr  7805  mulsrpr  7806  lttrsr  7822  mulgt0sr  7838  ltresr  7899  axpre-lttrn  7944  axpre-mulgt0  7947  recexgt0  8599  apreap  8606  apreim  8622  aprcl  8665  aptap  8669  prime  9416  rexuz  9645  ltxr  9841  ixxval  9962  fzval  10076  eqwrd  10954  sqrtrval  11144  abslt  11232  absle  11233  lenegsq  11239  abs2difabs  11252  2clim  11444  climcn2  11452  addcn2  11453  mulcn2  11455  climrecvg1n  11491  sumeq1  11498  fsum2dlemstep  11577  modfsummod  11601  prodeq1f  11695  fprod2dlemstep  11765  nndivdvds  11939  divalg2  12067  gcdval  12096  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlemex  12138  gcdass  12152  lcmval  12201  lcmass  12223  rpexp  12291  pythagtriplem2  12404  pythagtrip  12421  gsumfzval  12974  issgrpv  12987  issgrpn0  12988  ismhm  13033  mhmpropd  13038  issubm  13044  issubg  13243  issubg3  13262  ringpropd  13534  crngpropd  13535  opprunitd  13606  issubrg  13717  resrhm2b  13745  islmod  13787  lmodlema  13788  lmodprop2d  13844  islssm  13853  islssmg  13854  lsslss  13877  znleval  14141  psrbag  14155  istopg  14167  basis2  14216  tg2  14228  iscld  14271  neival  14311  isnei  14312  isneip  14314  iscn  14365  cnpval  14366  iscnp  14367  txbas  14426  txdis1cn  14446  ispsmet  14491  ismet  14512  isxmet  14513  ismet2  14522  blres  14602  elmopn  14614  mopni  14650  neibl  14659  metrest  14674  elcncf  14728  mulc1cncf  14744  mulcncf  14762  limccnp2lem  14830  sincosq2sgn  14962  sincosq4sgn  14964  bdsep2  15378  bdzfauscl  15382  bj-d0clsepcl  15417  sscoll2  15480