Theorem anbi2d 464

Description: Deduction adding a left 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
anbi2d	|- ( ph -> ( ( th /\ ps ) <-> ( th /\ ch ) ) )

Proof of Theorem anbi2d

Step	Hyp	Ref	Expression
1		anbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	a1d 22	. 2 |- ( ph -> ( th -> ( ps <-> ch ) ) )
3	2	pm5.32d 450	1 |- ( ph -> ( ( th /\ ps ) <-> ( th /\ ch ) ) )

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:  anbi2  467  anbi1cd  468  anbi12d  473  bi2anan9  606  dn1dc  962  xorbi2d  1391  dfbi3dc  1408  xordidc  1410  eleq2w  2258  eleq2  2260  ceqsex2  2804  ceqsex6v  2808  vtocl2gaf  2831  ceqsrex2v  2896  mob2  2944  eqreu  2956  nelrdva  2971  dfss4st  3397  undif4  3514  r19.27m  3547  ifbi  3582  preq12bg  3804  opeq2  3810  ralunsn  3828  intab  3904  disjiun  4029  brimralrspcev  4093  opabbid  4099  opthg  4272  pocl  4339  ordelord  4417  ordtriexmid  4558  ontr2exmid  4562  onsucsssucexmid  4564  tfisi  4624  xpeq2  4679  rabxp  4701  vtoclr  4712  opeliunxp  4719  posng  4736  opbrop  4743  rexiunxp  4809  elrnmpt1  4918  dfres2  4999  brcodir  5058  poltletr  5071  xp11m  5109  elxp4  5158  elxp5  5159  dffun4f  5275  fununi  5327  fneq2  5348  fnun  5367  feq3  5395  foeq3  5481  funfveu  5574  funbrfv  5602  ssimaexg  5626  fvopab3g  5637  fvopab3ig  5638  fvelrn  5696  fmptco  5731  fsn2  5739  elunirn  5816  isoeq2  5852  isoeq3  5853  isocnv2  5862  isoini  5868  isopolem  5872  f1oiso  5876  f1oiso2  5877  oprabbid  5979  cbvoprab3  6002  mpomptx  6017  mpofun  6028  ov  6046  ovi3  6064  ov6g  6065  ovg  6066  caoftrn  6172  uchoice  6204  f1o2ndf1  6295  xporderlem  6298  f1od2  6302  brtpos2  6318  brtposg  6321  dftpos4  6330  recseq  6373  tfrlem3-2d  6379  tfrlemi1  6399  tfrexlem  6401  tfr1onlemaccex  6415  tfrcllemaccex  6428  tfrcl  6431  freceq1  6459  freceq2  6460  frecsuc  6474  nnaordex  6595  brecop  6693  eroveu  6694  erovlem  6695  ecopovtrn  6700  ecopovtrng  6703  th3qlem1  6705  th3qlem2  6706  th3q  6708  elpmg  6732  ixpsnval  6769  ixpsnf1o  6804  domeng  6820  dom2lem  6840  xpcomco  6894  xpassen  6898  xpdom2  6899  xpf1o  6914  phplem3g  6926  ssfiexmid  6946  domfiexmid  6948  findcard2  6959  findcard2s  6960  findcard2d  6961  findcard2sd  6962  diffifi  6964  fiintim  7001  opabfi  7008  fidcenumlemrk  7029  fidcenumlemr  7030  supeq2  7064  nninfninc  7198  nnnninfeq2  7204  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  isacnm  7286  acfun  7290  2omotaplemap  7340  2omotaplemst  7341  exmidapne  7343  ccfunen  7347  recexnq  7474  recmulnqg  7475  ltsonq  7482  enq0sym  7516  enq0ref  7517  enq0tr  7518  enq0breq  7520  addnq0mo  7531  mulnq0mo  7532  addnnnq0  7533  mulnnnq0  7534  elinp  7558  prdisj  7576  prarloclem3  7581  prarloc  7587  distrlem5prl  7670  distrlem5pru  7671  ltexprlemell  7682  ltexprlemelu  7683  recexprlemm  7708  addsrmo  7827  mulsrmo  7828  addsrpr  7829  mulsrpr  7830  lttrsr  7846  recexgt0sr  7857  mulgt0sr  7862  ltresr  7923  axprecex  7964  axpre-lttrn  7968  axpre-mulgt0  7971  eqlelt  8130  lesub0  8523  apreap  8631  apreim  8647  aprcl  8690  aptap  8694  zltlen  9421  prime  9442  fzind  9458  qltlen  9731  xltnegi  9927  ixxval  9988  fzval  10102  fzdifsuc  10173  elfzm11  10183  elfzo  10241  zsupcllemex  10337  exbtwnzlemshrink  10355  rebtwn2zlemshrink  10360  facwordi  10849  zfz1iso  10950  shftfvalg  11000  shftfibg  11002  shftfval  11003  shftfib  11005  shftfn  11006  2shfti  11013  cau3lem  11296  caubnd2  11299  xrmaxiflemcom  11431  clim  11463  clim2  11465  climi  11469  climcn2  11491  addcn2  11492  subcn2  11493  mulcn2  11494  summodclem2a  11563  summodc  11565  fsum3  11569  fsumsplitf  11590  prodfdivap  11729  ntrivcvgap0  11731  prodeq1f  11734  prodeq2w  11738  prodeq2  11739  prodmodc  11760  zproddc  11761  fprodseq  11765  fprodntrivap  11766  fproddivapf  11813  fprodsplitf  11814  fprodsplit1f  11816  sinbnd  11934  cosbnd  11935  divalgb  12107  ndvdssub  12112  gcdval  12151  gcdneg  12174  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlemex  12193  dfgcd2  12206  gcdass  12207  algcvgblem  12242  lcmval  12256  lcmneg  12267  lcmgcdlem  12270  lcmass  12278  qredeq  12289  prmind2  12313  euclemma  12339  pw2dvdslemn  12358  qnumval  12378  qdenval  12379  pceu  12489  pczpre  12491  pcdiv  12496  prmpwdvds  12549  prdsex  12971  gsumpropd  13094  gsumpropd2  13095  gsumress  13097  gsum0g  13098  mnd1  13157  grp1  13308  qusgrp2  13319  nmznsg  13419  releqgg  13426  eqgex  13427  iscmnd  13504  issrg  13597  iscrng2  13647  qusring2  13698  opprunitd  13742  crngunit  13743  dfrhm2  13786  rhmopp  13808  issubrng  13831  resrhm2b  13881  islmod  13923  lsssetm  13988  lsspropdg  14063  ixpsnbasval  14098  basis2  14368  eltg2  14373  isnei  14464  isneip  14466  restbasg  14488  iscnp  14519  iscnp3  14523  tgcn  14528  icnpimaex  14531  lmbrf  14535  cncnp  14550  cnptoprest2  14560  txbas  14578  txcnp  14591  imasnopn  14619  ispsmet  14643  ismet  14664  isxmet  14665  ismet2  14674  blres  14754  metcnp3  14831  txmetcnp  14838  mulcncf  14928  ellimc3apf  14980  limcdifap  14982  limcmpted  14983  limccnp2lem  14996  dvmptfsum  15045  elply2  15055  sincosq3sgn  15148  lgsquadlem1  15402  2sqlem8  15448  2sqlem9  15449  subctctexmid  15731