Theorem anbi1d 469

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi1  470  anbi12d  477  bi2anan9  614  pm5.71dc  974  dfifp4dc  996  dfifp5dc  997  xorbi1d  1430  drsb1  1852  ax11ev  1881  eleq1w  2299  eleq1  2301  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  rabeqf  2811  vtocl2gaf  2890  alexeq  2952  ceqex  2953  elrabi  2979  sbc5  3075  rexss  3315  ineq1  3425  difin2  3493  r19.28m  3617  elif  3652  ifeqeqxdc  3687  rabsnifsb  3777  preq12bg  3898  opeq1  3904  eluni  3938  disjiun  4125  mpteq12f  4212  axsepg  4252  sepg  4253  zfausclOLD  4255  opthg  4380  copsexg  4386  euotd  4397  elopab  4402  pocl  4450  uniuni  4599  rabxfrd  4617  ontr2exmid  4674  regexmidlemm  4681  regexmidlem1  4682  reg2exmidlema  4683  preleq  4704  xpeq1  4790  elxpi  4792  vtoclr  4825  opbrop  4856  opelresg  5072  resopab2  5113  elxp4  5278  elxp5  5279  cnvpom  5333  fun11  5451  feq2  5520  f1eq2  5597  f1eq3  5598  foeq2  5615  brprcneu  5691  ssimaexg  5768  dmfco  5776  fndmdif  5817  respreima  5839  isoeq5  6014  isoini  6027  isopolem  6031  f1oiso  6035  f1oiso2  6036  riotaeqdv  6042  acexmidlemab  6082  acexmidlemcase  6083  oprabid  6120  mpoeq123  6150  mpoeq123dva  6152  eloprabga  6178  resoprab  6187  resoprab2  6188  ov  6211  ovi3  6229  ov6g  6230  ovg  6231  caoftrn  6339  opabex3d  6354  opabex3  6355  elxp7  6408  eloprabi  6436  cnvf1o  6465  xporderlem  6471  poxp  6472  rexsupp  6497  smoel2  6578  frec0g  6672  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecsuc  6682  nnaordex  6805  qliftel  6893  brecop  6903  eroveu  6904  ecopovtrn  6910  ecopovtrng  6913  th3qlem2  6916  th3q  6918  ixpsnf1o  7022  dom2lem  7062  mapsnend  7103  modom  7112  xpsnen  7123  xpassen  7132  pw2f1odclem  7138  xpf1o  7148  opabfi  7251  ctssdccl  7457  exmidapne  7632  dfplpq2  7727  dfmpq2  7728  ltsonq  7771  enq0sym  7805  enq0ref  7806  enq0tr  7807  enq0breq  7809  addnq0mo  7820  mulnq0mo  7821  addnnnq0  7822  mulnnnq0  7823  elinp  7847  prnmaxl  7861  prnminu  7862  prarloclemlo  7867  prarloc  7876  genpdflem  7880  genpassl  7897  genpassu  7898  ltexprlemm  7973  recexprlemell  7995  recexprlemelu  7996  cauappcvgprlemdisj  8024  caucvgprlemnkj  8039  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  addsrmo  8116  mulsrmo  8117  addsrpr  8118  mulsrpr  8119  lttrsr  8135  mulgt0sr  8151  ltresr  8212  axpre-lttrn  8257  axpre-mulgt0  8260  recexgt0  8916  apreap  8923  apreim  8939  aprcl  8982  aptap  8986  prime  9756  rexuz  9996  ltxr  10194  ixxval  10315  fzval  10430  hashfibclem  11304  hashf1lem2  11308  eqwrd  11367  pfxeq  11490  wrd2ind  11517  sqrtrval  11788  abslt  11877  absle  11878  lenegsq  11884  abs2difabs  11897  2clim  12092  climcn2  12100  addcn2  12101  mulcn2  12103  climrecvg1n  12139  sumeq1  12146  fsum2dlemstep  12226  modfsummod  12250  prodeq1f  12344  fprod2dlemstep  12414  nndivdvds  12588  divalg2  12718  gcdval  12761  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlemex  12803  gcdass  12817  lcmval  12866  lcmass  12888  rpexp  12957  pythagtriplem2  13074  pythagtrip  13091  gzsumfzval  13770  issgrpv  13778  issgrpn0  13779  ismhm  13827  mhmpropd  13832  issubm  13838  issubg  14035  issubg3  14054  ringpropd  14450  crngpropd  14451  opprunitd  14526  issubrg  14638  resrhm2b  14666  islmod  14736  lmodlema  14737  lmodprop2d  14794  islssm  14803  islssmg  14804  lsslss  14827  znleval  15097  psrbag  15162  istopg  15225  basis2  15274  tg2  15286  iscld  15329  neival  15369  isnei  15370  isneip  15372  iscn  15423  cnpval  15424  iscnp  15425  txbas  15484  txdis1cn  15504  ispsmet  15549  ismet  15570  isxmet  15571  ismet2  15580  blres  15660  elmopn  15672  mopni  15708  neibl  15717  metrest  15732  elcncf  15799  mulc1cncf  15815  mulcncf  15834  limccnp2lem  15902  sincosq2sgn  16054  sincosq4sgn  16056  pellexlem3  16231  bpos  16320  2lgslem1a  16412  edgssv2en  16645  uhgr2edg  16652  vtxdfifiun  16743  trlsfvalg  16829  istrl  16831  clwwlknp  16863  iseupth  16893  eupth2lem2dc  16905  bdsep2  17117  bdsepg  17121  bj-d0clsepcl  17156  sscoll2  17219  wexmiddifxy  17251