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  960  xorbi2d  1380  dfbi3dc  1397  xordidc  1399  eleq2w  2239  eleq2  2241  ceqsex2  2779  ceqsex6v  2783  vtocl2gaf  2806  ceqsrex2v  2871  mob2  2919  eqreu  2931  nelrdva  2946  dfss4st  3370  undif4  3487  r19.27m  3520  ifbi  3556  preq12bg  3775  opeq2  3781  ralunsn  3799  intab  3875  disjiun  4000  brimralrspcev  4064  opabbid  4070  opthg  4240  pocl  4305  ordelord  4383  ordtriexmid  4522  ontr2exmid  4526  onsucsssucexmid  4528  tfisi  4588  xpeq2  4643  rabxp  4665  vtoclr  4676  opeliunxp  4683  posng  4700  opbrop  4707  rexiunxp  4771  elrnmpt1  4880  dfres2  4961  brcodir  5018  poltletr  5031  xp11m  5069  elxp4  5118  elxp5  5119  dffun4f  5234  fununi  5286  fneq2  5307  fnun  5324  feq3  5352  foeq3  5438  funfveu  5530  funbrfv  5556  ssimaexg  5580  fvopab3g  5591  fvopab3ig  5592  fvelrn  5649  fmptco  5684  fsn2  5692  elunirn  5769  isoeq2  5805  isoeq3  5806  isocnv2  5815  isoini  5821  isopolem  5825  f1oiso  5829  f1oiso2  5830  oprabbid  5930  cbvoprab3  5953  mpomptx  5968  mpofun  5979  ov  5996  ovi3  6013  ov6g  6014  ovg  6015  caoftrn  6110  f1o2ndf1  6231  xporderlem  6234  f1od2  6238  brtpos2  6254  brtposg  6257  dftpos4  6266  recseq  6309  tfrlem3-2d  6315  tfrlemi1  6335  tfrexlem  6337  tfr1onlemaccex  6351  tfrcllemaccex  6364  tfrcl  6367  freceq1  6395  freceq2  6396  frecsuc  6410  nnaordex  6531  brecop  6627  eroveu  6628  erovlem  6629  ecopovtrn  6634  ecopovtrng  6637  th3qlem1  6639  th3qlem2  6640  th3q  6642  elpmg  6666  ixpsnval  6703  ixpsnf1o  6738  domeng  6754  dom2lem  6774  xpcomco  6828  xpassen  6832  xpdom2  6833  xpf1o  6846  phplem3g  6858  ssfiexmid  6878  domfiexmid  6880  findcard2  6891  findcard2s  6892  findcard2d  6893  findcard2sd  6894  diffifi  6896  fiintim  6930  fidcenumlemrk  6955  fidcenumlemr  6956  supeq2  6990  nnnninfeq2  7129  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  acfun  7208  2omotaplemap  7258  2omotaplemst  7259  exmidapne  7261  ccfunen  7265  recexnq  7391  recmulnqg  7392  ltsonq  7399  enq0sym  7433  enq0ref  7434  enq0tr  7435  enq0breq  7437  addnq0mo  7448  mulnq0mo  7449  addnnnq0  7450  mulnnnq0  7451  elinp  7475  prdisj  7493  prarloclem3  7498  prarloc  7504  distrlem5prl  7587  distrlem5pru  7588  ltexprlemell  7599  ltexprlemelu  7600  recexprlemm  7625  addsrmo  7744  mulsrmo  7745  addsrpr  7746  mulsrpr  7747  lttrsr  7763  recexgt0sr  7774  mulgt0sr  7779  ltresr  7840  axprecex  7881  axpre-lttrn  7885  axpre-mulgt0  7888  eqlelt  8046  lesub0  8438  apreap  8546  apreim  8562  aprcl  8605  aptap  8609  zltlen  9333  prime  9354  fzind  9370  qltlen  9642  xltnegi  9837  ixxval  9898  fzval  10012  fzdifsuc  10083  elfzm11  10093  elfzo  10151  exbtwnzlemshrink  10251  rebtwn2zlemshrink  10256  facwordi  10722  zfz1iso  10823  shftfvalg  10829  shftfibg  10831  shftfval  10832  shftfib  10834  shftfn  10835  2shfti  10842  cau3lem  11125  caubnd2  11128  xrmaxiflemcom  11259  clim  11291  clim2  11293  climi  11297  climcn2  11319  addcn2  11320  subcn2  11321  mulcn2  11322  summodclem2a  11391  summodc  11393  fsum3  11397  fsumsplitf  11418  prodfdivap  11557  ntrivcvgap0  11559  prodeq1f  11562  prodeq2w  11566  prodeq2  11567  prodmodc  11588  zproddc  11589  fprodseq  11593  fprodntrivap  11594  fproddivapf  11641  fprodsplitf  11642  fprodsplit1f  11644  sinbnd  11762  cosbnd  11763  divalgb  11932  ndvdssub  11937  zsupcllemex  11949  gcdval  11962  gcdneg  11985  bezoutlemstep  12000  bezoutlemmain  12001  bezoutlemex  12004  dfgcd2  12017  gcdass  12018  algcvgblem  12051  lcmval  12065  lcmneg  12076  lcmgcdlem  12079  lcmass  12087  qredeq  12098  prmind2  12122  euclemma  12148  pw2dvdslemn  12167  qnumval  12187  qdenval  12188  pceu  12297  pczpre  12299  pcdiv  12304  prmpwdvds  12355  prdsex  12723  mnd1  12852  grp1  12981  nmznsg  13078  releqgg  13085  iscmnd  13106  issrg  13153  iscrng2  13203  opprunitd  13284  crngunit  13285  islmod  13386  lsssetm  13449  basis2  13587  eltg2  13592  isnei  13683  isneip  13685  restbasg  13707  iscnp  13738  iscnp3  13742  tgcn  13747  icnpimaex  13750  lmbrf  13754  cncnp  13769  cnptoprest2  13779  txbas  13797  txcnp  13810  imasnopn  13838  ispsmet  13862  ismet  13883  isxmet  13884  ismet2  13893  blres  13973  metcnp3  14050  txmetcnp  14057  mulcncf  14130  ellimc3apf  14168  limcdifap  14170  limcmpted  14171  limccnp2lem  14184  sincosq3sgn  14288  2sqlem8  14509  2sqlem9  14510  subctctexmid  14789