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  1813  ax11ev  1842  eleq1w  2257  eleq1  2259  rexeqf  2690  reueq1f  2691  rmoeq1f  2692  rabeqf  2753  vtocl2gaf  2831  alexeq  2890  ceqex  2891  elrabi  2917  sbc5  3013  rexss  3250  ineq1  3357  difin2  3425  r19.28m  3540  preq12bg  3803  opeq1  3808  eluni  3842  disjiun  4028  mpteq12f  4113  axsep2  4152  zfauscl  4153  opthg  4271  copsexg  4277  euotd  4287  elopab  4292  pocl  4338  uniuni  4486  rabxfrd  4504  ontr2exmid  4561  regexmidlemm  4568  regexmidlem1  4569  reg2exmidlema  4570  preleq  4591  xpeq1  4677  elxpi  4679  vtoclr  4711  opbrop  4742  opelresg  4953  resopab2  4993  elxp4  5157  elxp5  5158  cnvpom  5212  fun11  5325  feq2  5391  f1eq2  5459  f1eq3  5460  foeq2  5477  brprcneu  5551  ssimaexg  5623  dmfco  5629  fndmdif  5667  rexsupp  5686  respreima  5690  isoeq5  5852  isoini  5865  isopolem  5869  f1oiso  5873  f1oiso2  5874  riotaeqdv  5878  acexmidlemab  5916  acexmidlemcase  5917  oprabid  5954  mpoeq123  5981  mpoeq123dva  5983  eloprabga  6009  resoprab  6018  resoprab2  6019  ov  6042  ovi3  6060  ov6g  6061  ovg  6062  caoftrn  6163  opabex3d  6178  opabex3  6179  elxp7  6228  eloprabi  6254  cnvf1o  6283  xporderlem  6289  poxp  6290  smoel2  6361  frec0g  6455  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecsuc  6465  nnaordex  6586  qliftel  6674  brecop  6684  eroveu  6685  ecopovtrn  6691  ecopovtrng  6694  th3qlem2  6697  th3q  6699  ixpsnf1o  6795  dom2lem  6831  xpsnen  6880  xpassen  6889  pw2f1odclem  6895  xpf1o  6905  opabfi  6999  ctssdccl  7177  exmidapne  7327  dfplpq2  7421  dfmpq2  7422  ltsonq  7465  enq0sym  7499  enq0ref  7500  enq0tr  7501  enq0breq  7503  addnq0mo  7514  mulnq0mo  7515  addnnnq0  7516  mulnnnq0  7517  elinp  7541  prnmaxl  7555  prnminu  7556  prarloclemlo  7561  prarloc  7570  genpdflem  7574  genpassl  7591  genpassu  7592  ltexprlemm  7667  recexprlemell  7689  recexprlemelu  7690  cauappcvgprlemdisj  7718  caucvgprlemnkj  7733  caucvgprprlemnkltj  7756  caucvgprprlemnkeqj  7757  addsrmo  7810  mulsrmo  7811  addsrpr  7812  mulsrpr  7813  lttrsr  7829  mulgt0sr  7845  ltresr  7906  axpre-lttrn  7951  axpre-mulgt0  7954  recexgt0  8607  apreap  8614  apreim  8630  aprcl  8673  aptap  8677  prime  9425  rexuz  9654  ltxr  9850  ixxval  9971  fzval  10085  eqwrd  10975  sqrtrval  11165  abslt  11253  absle  11254  lenegsq  11260  abs2difabs  11273  2clim  11466  climcn2  11474  addcn2  11475  mulcn2  11477  climrecvg1n  11513  sumeq1  11520  fsum2dlemstep  11599  modfsummod  11623  prodeq1f  11717  fprod2dlemstep  11787  nndivdvds  11961  divalg2  12091  gcdval  12126  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlemex  12168  gcdass  12182  lcmval  12231  lcmass  12253  rpexp  12321  pythagtriplem2  12435  pythagtrip  12452  gsumfzval  13034  issgrpv  13047  issgrpn0  13048  ismhm  13093  mhmpropd  13098  issubm  13104  issubg  13303  issubg3  13322  ringpropd  13594  crngpropd  13595  opprunitd  13666  issubrg  13777  resrhm2b  13805  islmod  13847  lmodlema  13848  lmodprop2d  13904  islssm  13913  islssmg  13914  lsslss  13937  znleval  14209  psrbag  14223  istopg  14235  basis2  14284  tg2  14296  iscld  14339  neival  14379  isnei  14380  isneip  14382  iscn  14433  cnpval  14434  iscnp  14435  txbas  14494  txdis1cn  14514  ispsmet  14559  ismet  14580  isxmet  14581  ismet2  14590  blres  14670  elmopn  14682  mopni  14718  neibl  14727  metrest  14742  elcncf  14809  mulc1cncf  14825  mulcncf  14844  limccnp2lem  14912  sincosq2sgn  15063  sincosq4sgn  15065  2lgslem1a  15329  bdsep2  15532  bdzfauscl  15536  bj-d0clsepcl  15571  sscoll2  15634