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  963  xorbi2d  1400  dfbi3dc  1417  xordidc  1419  eleq2w  2267  eleq2  2269  ceqsex2  2813  ceqsex6v  2817  vtocl2gaf  2840  ceqsrex2v  2905  mob2  2953  eqreu  2965  nelrdva  2980  dfss4st  3406  undif4  3523  r19.27m  3556  ifbi  3591  preq12bg  3814  opeq2  3820  ralunsn  3838  intab  3914  disjiun  4040  brimralrspcev  4104  opabbid  4110  opthg  4283  pocl  4351  ordelord  4429  ordtriexmid  4570  ontr2exmid  4574  onsucsssucexmid  4576  tfisi  4636  xpeq2  4691  rabxp  4713  vtoclr  4724  opeliunxp  4731  posng  4748  opbrop  4755  rexiunxp  4821  elrnmpt1  4930  dfres2  5012  brcodir  5071  poltletr  5084  xp11m  5122  elxp4  5171  elxp5  5172  dffun4f  5288  fununi  5343  fneq2  5364  fnun  5383  feq3  5412  foeq3  5498  funfveu  5591  funbrfv  5619  ssimaexg  5643  fvopab3g  5654  fvopab3ig  5655  fvelrn  5713  fmptco  5748  fsn2  5756  elunirn  5837  isoeq2  5873  isoeq3  5874  isocnv2  5883  isoini  5889  isopolem  5893  f1oiso  5897  f1oiso2  5898  oprabbid  6000  cbvoprab3  6023  mpomptx  6038  mpofun  6049  ov  6067  ovi3  6085  ov6g  6086  ovg  6087  caoftrn  6193  uchoice  6225  f1o2ndf1  6316  xporderlem  6319  f1od2  6323  brtpos2  6339  brtposg  6342  dftpos4  6351  recseq  6394  tfrlem3-2d  6400  tfrlemi1  6420  tfrexlem  6422  tfr1onlemaccex  6436  tfrcllemaccex  6449  tfrcl  6452  freceq1  6480  freceq2  6481  frecsuc  6495  nnaordex  6616  brecop  6714  eroveu  6715  erovlem  6716  ecopovtrn  6721  ecopovtrng  6724  th3qlem1  6726  th3qlem2  6727  th3q  6729  elpmg  6753  ixpsnval  6790  ixpsnf1o  6825  domeng  6843  dom2lem  6865  xpcomco  6923  xpassen  6927  xpdom2  6928  xpf1o  6943  phplem3g  6955  ssfiexmid  6975  domfiexmid  6977  findcard2  6988  findcard2s  6989  findcard2d  6990  findcard2sd  6991  diffifi  6993  fiintim  7030  opabfi  7037  fidcenumlemrk  7058  fidcenumlemr  7059  supeq2  7093  nninfninc  7227  nnnninfeq2  7233  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  isacnm  7317  acfun  7321  2omotaplemap  7371  2omotaplemst  7372  exmidapne  7374  ccfunen  7378  recexnq  7505  recmulnqg  7506  ltsonq  7513  enq0sym  7547  enq0ref  7548  enq0tr  7549  enq0breq  7551  addnq0mo  7562  mulnq0mo  7563  addnnnq0  7564  mulnnnq0  7565  elinp  7589  prdisj  7607  prarloclem3  7612  prarloc  7618  distrlem5prl  7701  distrlem5pru  7702  ltexprlemell  7713  ltexprlemelu  7714  recexprlemm  7739  addsrmo  7858  mulsrmo  7859  addsrpr  7860  mulsrpr  7861  lttrsr  7877  recexgt0sr  7888  mulgt0sr  7893  ltresr  7954  axprecex  7995  axpre-lttrn  7999  axpre-mulgt0  8002  eqlelt  8161  lesub0  8554  apreap  8662  apreim  8678  aprcl  8721  aptap  8725  zltlen  9453  prime  9474  fzind  9490  qltlen  9763  xltnegi  9959  ixxval  10020  fzval  10134  fzdifsuc  10205  elfzm11  10215  elfzo  10273  zsupcllemex  10375  exbtwnzlemshrink  10393  rebtwn2zlemshrink  10398  facwordi  10887  zfz1iso  10988  pfxsuff1eqwrdeq  11153  shftfvalg  11162  shftfibg  11164  shftfval  11165  shftfib  11167  shftfn  11168  2shfti  11175  cau3lem  11458  caubnd2  11461  xrmaxiflemcom  11593  clim  11625  clim2  11627  climi  11631  climcn2  11653  addcn2  11654  subcn2  11655  mulcn2  11656  summodclem2a  11725  summodc  11727  fsum3  11731  fsumsplitf  11752  prodfdivap  11891  ntrivcvgap0  11893  prodeq1f  11896  prodeq2w  11900  prodeq2  11901  prodmodc  11922  zproddc  11923  fprodseq  11927  fprodntrivap  11928  fproddivapf  11975  fprodsplitf  11976  fprodsplit1f  11978  sinbnd  12096  cosbnd  12097  divalgb  12269  ndvdssub  12274  gcdval  12313  gcdneg  12336  bezoutlemstep  12351  bezoutlemmain  12352  bezoutlemex  12355  dfgcd2  12368  gcdass  12369  algcvgblem  12404  lcmval  12418  lcmneg  12429  lcmgcdlem  12432  lcmass  12440  qredeq  12451  prmind2  12475  euclemma  12501  pw2dvdslemn  12520  qnumval  12540  qdenval  12541  pceu  12651  pczpre  12653  pcdiv  12658  prmpwdvds  12711  prdsex  13134  gsumpropd  13257  gsumpropd2  13258  gsumress  13260  gsum0g  13261  mnd1  13320  grp1  13471  qusgrp2  13482  nmznsg  13582  releqgg  13589  eqgex  13590  iscmnd  13667  issrg  13760  iscrng2  13810  qusring2  13861  opprunitd  13905  crngunit  13906  dfrhm2  13949  rhmopp  13971  issubrng  13994  resrhm2b  14044  islmod  14086  lsssetm  14151  lsspropdg  14226  ixpsnbasval  14261  basis2  14553  eltg2  14558  isnei  14649  isneip  14651  restbasg  14673  iscnp  14704  iscnp3  14708  tgcn  14713  icnpimaex  14716  lmbrf  14720  cncnp  14735  cnptoprest2  14745  txbas  14763  txcnp  14776  imasnopn  14804  ispsmet  14828  ismet  14849  isxmet  14850  ismet2  14859  blres  14939  metcnp3  15016  txmetcnp  15023  mulcncf  15113  ellimc3apf  15165  limcdifap  15167  limcmpted  15168  limccnp2lem  15181  dvmptfsum  15230  elply2  15240  sincosq3sgn  15333  lgsquadlem1  15587  2sqlem8  15633  2sqlem9  15634  subctctexmid  15974  nnnninfex  15996