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  961  xorbi1d  1381  drsb1  1799  ax11ev  1828  eleq1w  2238  eleq1  2240  rexeqf  2670  reueq1f  2671  rmoeq1f  2672  rabeqf  2728  vtocl2gaf  2805  alexeq  2864  ceqex  2865  elrabi  2891  sbc5  2987  rexss  3223  ineq1  3330  difin2  3398  r19.28m  3513  preq12bg  3774  opeq1  3779  eluni  3813  disjiun  3999  mpteq12f  4084  axsep2  4123  zfauscl  4124  opthg  4239  copsexg  4245  euotd  4255  elopab  4259  pocl  4304  uniuni  4452  rabxfrd  4470  ontr2exmid  4525  regexmidlemm  4532  regexmidlem1  4533  reg2exmidlema  4534  preleq  4555  xpeq1  4641  elxpi  4643  vtoclr  4675  opbrop  4706  opelresg  4915  resopab2  4955  elxp4  5117  elxp5  5118  cnvpom  5172  fun11  5284  feq2  5350  f1eq2  5418  f1eq3  5419  foeq2  5436  brprcneu  5509  ssimaexg  5579  dmfco  5585  fndmdif  5622  rexsupp  5641  respreima  5645  isoeq5  5806  isoini  5819  isopolem  5823  f1oiso  5827  f1oiso2  5828  riotaeqdv  5832  acexmidlemab  5869  acexmidlemcase  5870  oprabid  5907  mpoeq123  5934  mpoeq123dva  5936  eloprabga  5962  resoprab  5971  resoprab2  5972  ov  5994  ovi3  6011  ov6g  6012  ovg  6013  caoftrn  6108  opabex3d  6122  opabex3  6123  elxp7  6171  eloprabi  6197  cnvf1o  6226  xporderlem  6232  poxp  6233  smoel2  6304  frec0g  6398  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecsuc  6408  nnaordex  6529  qliftel  6615  brecop  6625  eroveu  6626  ecopovtrn  6632  ecopovtrng  6635  th3qlem2  6638  th3q  6640  ixpsnf1o  6736  dom2lem  6772  xpsnen  6821  xpassen  6830  xpf1o  6844  ctssdccl  7110  exmidapne  7259  dfplpq2  7353  dfmpq2  7354  ltsonq  7397  enq0sym  7431  enq0ref  7432  enq0tr  7433  enq0breq  7435  addnq0mo  7446  mulnq0mo  7447  addnnnq0  7448  mulnnnq0  7449  elinp  7473  prnmaxl  7487  prnminu  7488  prarloclemlo  7493  prarloc  7502  genpdflem  7506  genpassl  7523  genpassu  7524  ltexprlemm  7599  recexprlemell  7621  recexprlemelu  7622  cauappcvgprlemdisj  7650  caucvgprlemnkj  7665  caucvgprprlemnkltj  7688  caucvgprprlemnkeqj  7689  addsrmo  7742  mulsrmo  7743  addsrpr  7744  mulsrpr  7745  lttrsr  7761  mulgt0sr  7777  ltresr  7838  axpre-lttrn  7883  axpre-mulgt0  7886  recexgt0  8537  apreap  8544  apreim  8560  aprcl  8603  aptap  8607  prime  9352  rexuz  9580  ltxr  9775  ixxval  9896  fzval  10010  sqrtrval  11009  abslt  11097  absle  11098  lenegsq  11104  abs2difabs  11117  2clim  11309  climcn2  11317  addcn2  11318  mulcn2  11320  climrecvg1n  11356  sumeq1  11363  fsum2dlemstep  11442  modfsummod  11466  prodeq1f  11560  fprod2dlemstep  11630  nndivdvds  11803  divalg2  11931  gcdval  11960  bezoutlemstep  11998  bezoutlemmain  11999  bezoutlemex  12002  gcdass  12016  lcmval  12063  lcmass  12085  rpexp  12153  pythagtriplem2  12266  pythagtrip  12283  issgrpv  12810  issgrpn0  12811  ismhm  12853  mhmpropd  12857  issubm  12863  issubg  13033  issubg3  13052  ringpropd  13217  crngpropd  13218  opprunitd  13279  issubrg  13342  islmod  13381  lmodlema  13382  lmodprop2d  13438  istopg  13502  basis2  13551  tg2  13563  iscld  13606  neival  13646  isnei  13647  isneip  13649  iscn  13700  cnpval  13701  iscnp  13702  txbas  13761  txdis1cn  13781  ispsmet  13826  ismet  13847  isxmet  13848  ismet2  13857  blres  13937  elmopn  13949  mopni  13985  neibl  13994  metrest  14009  elcncf  14063  mulc1cncf  14079  mulcncf  14094  limccnp2lem  14148  sincosq2sgn  14251  sincosq4sgn  14253  bdsep2  14641  bdzfauscl  14645  bj-d0clsepcl  14680  sscoll2  14743