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  610  dn1dc  969  dfifp3dc  991  ifpdfbidc  994  xorbi2d  1425  dfbi3dc  1442  xordidc  1444  eleq2w  2293  eleq2  2295  ceqsex2  2845  ceqsex6v  2849  vtocl2gaf  2872  ceqsrex2v  2939  mob2  2987  eqreu  2999  nelrdva  3014  dfss4st  3442  undif4  3559  r19.27m  3592  ifbi  3630  preq12bg  3861  opeq2  3868  ralunsn  3886  intab  3962  disjiun  4088  brimralrspcev  4153  opabbid  4159  opthg  4336  pocl  4406  ordelord  4484  ordtriexmid  4625  ontr2exmid  4629  onsucsssucexmid  4631  tfisi  4691  xpeq2  4746  rabxp  4769  vtoclr  4780  opeliunxp  4787  posng  4804  opbrop  4811  rexiunxp  4878  elrnmpt1  4989  dfres2  5071  brcodir  5131  poltletr  5144  xp11m  5182  elxp4  5231  elxp5  5232  dffun4f  5349  fununi  5405  fneq2  5426  fnun  5445  feq3  5474  foeq3  5566  funfveu  5661  funbrfv  5691  ssimaexg  5717  fvopab3g  5728  fvopab3ig  5729  fvelrn  5786  fmptco  5821  fsn2  5829  elunirn  5917  isoeq2  5953  isoeq3  5954  isocnv2  5963  isoini  5969  isopolem  5973  f1oiso  5977  f1oiso2  5978  oprabbid  6084  cbvoprab3  6107  mpomptx  6122  mpofun  6133  ov  6151  ovi3  6169  ov6g  6170  ovg  6171  caoftrn  6277  uchoice  6309  f1o2ndf1  6402  xporderlem  6405  f1od2  6409  suppimacnvfn  6424  brtpos2  6460  brtposg  6463  dftpos4  6472  recseq  6515  tfrlem3-2d  6521  tfrlemi1  6541  tfrexlem  6543  tfr1onlemaccex  6557  tfrcllemaccex  6570  tfrcl  6573  freceq1  6601  freceq2  6602  frecsuc  6616  nnaordex  6739  brecop  6837  eroveu  6838  erovlem  6839  ecopovtrn  6844  ecopovtrng  6847  th3qlem1  6849  th3qlem2  6850  th3q  6852  elpmg  6876  ixpsnval  6913  ixpsnf1o  6948  domeng  6966  dom2lem  6988  modom  7037  xpcomco  7053  xpassen  7057  xpdom2  7058  xpf1o  7073  phplem3g  7085  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  findcard2  7121  findcard2s  7122  findcard2d  7123  findcard2sd  7124  diffifi  7126  fiintim  7166  opabfi  7175  fidcenumlemrk  7196  fidcenumlemr  7197  supeq2  7248  nninfninc  7382  nnnninfeq2  7388  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  isacnm  7478  acfun  7482  2omotaplemap  7536  2omotaplemst  7537  exmidapne  7539  ccfunen  7543  recexnq  7670  recmulnqg  7671  ltsonq  7678  enq0sym  7712  enq0ref  7713  enq0tr  7714  enq0breq  7716  addnq0mo  7727  mulnq0mo  7728  addnnnq0  7729  mulnnnq0  7730  elinp  7754  prdisj  7772  prarloclem3  7777  prarloc  7783  distrlem5prl  7866  distrlem5pru  7867  ltexprlemell  7878  ltexprlemelu  7879  recexprlemm  7904  addsrmo  8023  mulsrmo  8024  addsrpr  8025  mulsrpr  8026  lttrsr  8042  recexgt0sr  8053  mulgt0sr  8058  ltresr  8119  axprecex  8160  axpre-lttrn  8164  axpre-mulgt0  8167  eqlelt  8325  lesub0  8718  apreap  8826  apreim  8842  aprcl  8885  aptap  8889  zltlen  9619  prime  9640  fzind  9656  qltlen  9935  xltnegi  10131  ixxval  10192  fzval  10307  fzdifsuc  10378  elfzm11  10388  elfzo  10446  zsupcllemex  10553  exbtwnzlemshrink  10571  rebtwn2zlemshrink  10576  facwordi  11065  zfz1iso  11168  pfxsuff1eqwrdeq  11346  wrd2ind  11370  shftfvalg  11458  shftfibg  11460  shftfval  11461  shftfib  11463  shftfn  11464  2shfti  11471  cau3lem  11754  caubnd2  11757  xrmaxiflemcom  11889  clim  11921  clim2  11923  climi  11927  climcn2  11949  addcn2  11950  subcn2  11951  mulcn2  11952  summodclem2a  12022  summodc  12024  fsum3  12028  fsumsplitf  12049  prodfdivap  12188  ntrivcvgap0  12190  prodeq1f  12193  prodeq2w  12197  prodeq2  12198  prodmodc  12219  zproddc  12220  fprodseq  12224  fprodntrivap  12225  fproddivapf  12272  fprodsplitf  12273  fprodsplit1f  12275  sinbnd  12393  cosbnd  12394  divalgb  12566  ndvdssub  12571  gcdval  12610  gcdneg  12633  bezoutlemstep  12648  bezoutlemmain  12649  bezoutlemex  12652  dfgcd2  12665  gcdass  12666  algcvgblem  12701  lcmval  12715  lcmneg  12726  lcmgcdlem  12729  lcmass  12737  qredeq  12748  prmind2  12772  euclemma  12798  pw2dvdslemn  12817  qnumval  12837  qdenval  12838  pceu  12948  pczpre  12950  pcdiv  12955  prmpwdvds  13008  prdsex  13432  gsumpropd  13555  gsumpropd2  13556  gsumress  13558  gsum0g  13559  mnd1  13618  grp1  13769  qusgrp2  13780  nmznsg  13880  releqgg  13887  eqgex  13888  iscmnd  13965  issrg  14059  iscrng2  14109  qusring2  14160  opprunitd  14205  crngunit  14206  dfrhm2  14249  rhmopp  14271  issubrng  14294  resrhm2b  14344  islmod  14387  lsssetm  14452  lsspropdg  14527  ixpsnbasval  14562  basis2  14859  eltg2  14864  isnei  14955  isneip  14957  restbasg  14979  iscnp  15010  iscnp3  15014  tgcn  15019  icnpimaex  15022  lmbrf  15026  cncnp  15041  cnptoprest2  15051  txbas  15069  txcnp  15082  imasnopn  15110  ispsmet  15134  ismet  15155  isxmet  15156  ismet2  15165  blres  15245  metcnp3  15322  txmetcnp  15329  mulcncf  15419  ellimc3apf  15471  limcdifap  15473  limcmpted  15474  limccnp2lem  15487  dvmptfsum  15536  elply2  15546  sincosq3sgn  15639  pellexlem3  15793  lgsquadlem1  15896  2sqlem8  15942  2sqlem9  15943  eupthres  16398  eupth2lem3lem6fi  16412  subctctexmid  16722  nnnninfex  16748  gfsumval  16809