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 ) ) )

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  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  3614  elif  3649  ifeqeqxdc  3684  rabsnifsb  3773  preq12bg  3893  opeq1  3899  eluni  3933  disjiun  4120  mpteq12f  4206  axsepg  4245  sepg  4246  zfausclOLD  4248  opthg  4373  copsexg  4379  euotd  4390  elopab  4395  pocl  4443  uniuni  4592  rabxfrd  4610  ontr2exmid  4667  regexmidlemm  4674  regexmidlem1  4675  reg2exmidlema  4676  preleq  4697  xpeq1  4783  elxpi  4785  vtoclr  4818  opbrop  4849  opelresg  5065  resopab2  5105  elxp4  5270  elxp5  5271  cnvpom  5325  fun11  5443  feq2  5512  f1eq2  5589  f1eq3  5590  foeq2  5607  brprcneu  5683  ssimaexg  5759  dmfco  5767  fndmdif  5805  respreima  5827  isoeq5  6001  isoini  6014  isopolem  6018  f1oiso  6022  f1oiso2  6023  riotaeqdv  6029  acexmidlemab  6069  acexmidlemcase  6070  oprabid  6107  mpoeq123  6137  mpoeq123dva  6139  eloprabga  6165  resoprab  6174  resoprab2  6175  ov  6198  ovi3  6216  ov6g  6217  ovg  6218  caoftrn  6325  opabex3d  6340  opabex3  6341  elxp7  6394  eloprabi  6422  cnvf1o  6451  xporderlem  6457  poxp  6458  rexsupp  6483  smoel2  6564  frec0g  6658  freccllem  6663  frecfcllem  6665  frecsuclem  6667  frecsuc  6668  nnaordex  6791  qliftel  6879  brecop  6889  eroveu  6890  ecopovtrn  6896  ecopovtrng  6899  th3qlem2  6902  th3q  6904  ixpsnf1o  7008  dom2lem  7048  mapsnend  7089  modom  7098  xpsnen  7109  xpassen  7118  pw2f1odclem  7124  xpf1o  7134  opabfi  7237  ctssdccl  7441  exmidapne  7616  dfplpq2  7711  dfmpq2  7712  ltsonq  7755  enq0sym  7789  enq0ref  7790  enq0tr  7791  enq0breq  7793  addnq0mo  7804  mulnq0mo  7805  addnnnq0  7806  mulnnnq0  7807  elinp  7831  prnmaxl  7845  prnminu  7846  prarloclemlo  7851  prarloc  7860  genpdflem  7864  genpassl  7881  genpassu  7882  ltexprlemm  7957  recexprlemell  7979  recexprlemelu  7980  cauappcvgprlemdisj  8008  caucvgprlemnkj  8023  caucvgprprlemnkltj  8046  caucvgprprlemnkeqj  8047  addsrmo  8100  mulsrmo  8101  addsrpr  8102  mulsrpr  8103  lttrsr  8119  mulgt0sr  8135  ltresr  8196  axpre-lttrn  8241  axpre-mulgt0  8244  recexgt0  8898  apreap  8905  apreim  8921  aprcl  8964  aptap  8968  prime  9724  rexuz  9959  ltxr  10156  ixxval  10277  fzval  10392  hashfibclem  11260  hashf1lem2  11264  eqwrd  11323  pfxeq  11446  wrd2ind  11473  sqrtrval  11744  abslt  11832  absle  11833  lenegsq  11839  abs2difabs  11852  2clim  12045  climcn2  12053  addcn2  12054  mulcn2  12056  climrecvg1n  12092  sumeq1  12099  fsum2dlemstep  12179  modfsummod  12203  prodeq1f  12297  fprod2dlemstep  12367  nndivdvds  12541  divalg2  12671  gcdval  12714  bezoutlemstep  12752  bezoutlemmain  12753  bezoutlemex  12756  gcdass  12770  lcmval  12819  lcmass  12841  rpexp  12909  pythagtriplem2  13023  pythagtrip  13040  gzsumfzval  13688  issgrpv  13696  issgrpn0  13697  ismhm  13745  mhmpropd  13750  issubm  13756  issubg  13953  issubg3  13972  ringpropd  14316  crngpropd  14317  opprunitd  14390  issubrg  14502  resrhm2b  14530  islmod  14600  lmodlema  14601  lmodprop2d  14657  islssm  14666  islssmg  14667  lsslss  14690  znleval  14960  psrbag  14976  istopg  15023  basis2  15072  tg2  15084  iscld  15127  neival  15167  isnei  15168  isneip  15170  iscn  15221  cnpval  15222  iscnp  15223  txbas  15282  txdis1cn  15302  ispsmet  15347  ismet  15368  isxmet  15369  ismet2  15378  blres  15458  elmopn  15470  mopni  15506  neibl  15515  metrest  15530  elcncf  15597  mulc1cncf  15613  mulcncf  15632  limccnp2lem  15700  sincosq2sgn  15851  sincosq4sgn  15853  pellexlem3  16007  2lgslem1a  16121  edgssv2en  16354  uhgr2edg  16361  vtxdfifiun  16452  trlsfvalg  16538  istrl  16540  clwwlknp  16572  iseupth  16602  eupth2lem2dc  16614  bdsep2  16826  bdsepg  16830  bj-d0clsepcl  16865  sscoll2  16928