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  3396  undif4  3513  r19.27m  3546  ifbi  3581  preq12bg  3803  opeq2  3809  ralunsn  3827  intab  3903  disjiun  4028  brimralrspcev  4092  opabbid  4098  opthg  4271  pocl  4338  ordelord  4416  ordtriexmid  4557  ontr2exmid  4561  onsucsssucexmid  4563  tfisi  4623  xpeq2  4678  rabxp  4700  vtoclr  4711  opeliunxp  4718  posng  4735  opbrop  4742  rexiunxp  4808  elrnmpt1  4917  dfres2  4998  brcodir  5057  poltletr  5070  xp11m  5108  elxp4  5157  elxp5  5158  dffun4f  5274  fununi  5326  fneq2  5347  fnun  5364  feq3  5392  foeq3  5478  funfveu  5571  funbrfv  5599  ssimaexg  5623  fvopab3g  5634  fvopab3ig  5635  fvelrn  5693  fmptco  5728  fsn2  5736  elunirn  5813  isoeq2  5849  isoeq3  5850  isocnv2  5859  isoini  5865  isopolem  5869  f1oiso  5873  f1oiso2  5874  oprabbid  5975  cbvoprab3  5998  mpomptx  6013  mpofun  6024  ov  6042  ovi3  6060  ov6g  6061  ovg  6062  caoftrn  6163  uchoice  6195  f1o2ndf1  6286  xporderlem  6289  f1od2  6293  brtpos2  6309  brtposg  6312  dftpos4  6321  recseq  6364  tfrlem3-2d  6370  tfrlemi1  6390  tfrexlem  6392  tfr1onlemaccex  6406  tfrcllemaccex  6419  tfrcl  6422  freceq1  6450  freceq2  6451  frecsuc  6465  nnaordex  6586  brecop  6684  eroveu  6685  erovlem  6686  ecopovtrn  6691  ecopovtrng  6694  th3qlem1  6696  th3qlem2  6697  th3q  6699  elpmg  6723  ixpsnval  6760  ixpsnf1o  6795  domeng  6811  dom2lem  6831  xpcomco  6885  xpassen  6889  xpdom2  6890  xpf1o  6905  phplem3g  6917  ssfiexmid  6937  domfiexmid  6939  findcard2  6950  findcard2s  6951  findcard2d  6952  findcard2sd  6953  diffifi  6955  fiintim  6992  opabfi  6999  fidcenumlemrk  7020  fidcenumlemr  7021  supeq2  7055  nninfninc  7189  nnnninfeq2  7195  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  acfun  7274  2omotaplemap  7324  2omotaplemst  7325  exmidapne  7327  ccfunen  7331  recexnq  7457  recmulnqg  7458  ltsonq  7465  enq0sym  7499  enq0ref  7500  enq0tr  7501  enq0breq  7503  addnq0mo  7514  mulnq0mo  7515  addnnnq0  7516  mulnnnq0  7517  elinp  7541  prdisj  7559  prarloclem3  7564  prarloc  7570  distrlem5prl  7653  distrlem5pru  7654  ltexprlemell  7665  ltexprlemelu  7666  recexprlemm  7691  addsrmo  7810  mulsrmo  7811  addsrpr  7812  mulsrpr  7813  lttrsr  7829  recexgt0sr  7840  mulgt0sr  7845  ltresr  7906  axprecex  7947  axpre-lttrn  7951  axpre-mulgt0  7954  eqlelt  8113  lesub0  8506  apreap  8614  apreim  8630  aprcl  8673  aptap  8677  zltlen  9404  prime  9425  fzind  9441  qltlen  9714  xltnegi  9910  ixxval  9971  fzval  10085  fzdifsuc  10156  elfzm11  10166  elfzo  10224  zsupcllemex  10320  exbtwnzlemshrink  10338  rebtwn2zlemshrink  10343  facwordi  10832  zfz1iso  10933  shftfvalg  10983  shftfibg  10985  shftfval  10986  shftfib  10988  shftfn  10989  2shfti  10996  cau3lem  11279  caubnd2  11282  xrmaxiflemcom  11414  clim  11446  clim2  11448  climi  11452  climcn2  11474  addcn2  11475  subcn2  11476  mulcn2  11477  summodclem2a  11546  summodc  11548  fsum3  11552  fsumsplitf  11573  prodfdivap  11712  ntrivcvgap0  11714  prodeq1f  11717  prodeq2w  11721  prodeq2  11722  prodmodc  11743  zproddc  11744  fprodseq  11748  fprodntrivap  11749  fproddivapf  11796  fprodsplitf  11797  fprodsplit1f  11799  sinbnd  11917  cosbnd  11918  divalgb  12090  ndvdssub  12095  gcdval  12126  gcdneg  12149  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlemex  12168  dfgcd2  12181  gcdass  12182  algcvgblem  12217  lcmval  12231  lcmneg  12242  lcmgcdlem  12245  lcmass  12253  qredeq  12264  prmind2  12288  euclemma  12314  pw2dvdslemn  12333  qnumval  12353  qdenval  12354  pceu  12464  pczpre  12466  pcdiv  12471  prmpwdvds  12524  prdsex  12940  gsumpropd  13035  gsumpropd2  13036  gsumress  13038  gsum0g  13039  mnd1  13087  grp1  13238  qusgrp2  13243  nmznsg  13343  releqgg  13350  eqgex  13351  iscmnd  13428  issrg  13521  iscrng2  13571  qusring2  13622  opprunitd  13666  crngunit  13667  dfrhm2  13710  rhmopp  13732  issubrng  13755  resrhm2b  13805  islmod  13847  lsssetm  13912  lsspropdg  13987  ixpsnbasval  14022  basis2  14284  eltg2  14289  isnei  14380  isneip  14382  restbasg  14404  iscnp  14435  iscnp3  14439  tgcn  14444  icnpimaex  14447  lmbrf  14451  cncnp  14466  cnptoprest2  14476  txbas  14494  txcnp  14507  imasnopn  14535  ispsmet  14559  ismet  14580  isxmet  14581  ismet2  14590  blres  14670  metcnp3  14747  txmetcnp  14754  mulcncf  14844  ellimc3apf  14896  limcdifap  14898  limcmpted  14899  limccnp2lem  14912  dvmptfsum  14961  elply2  14971  sincosq3sgn  15064  lgsquadlem1  15318  2sqlem8  15364  2sqlem9  15365  subctctexmid  15645