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  608  dn1dc  966  dfifp3dc  988  ifpdfbidc  991  xorbi2d  1422  dfbi3dc  1439  xordidc  1441  eleq2w  2291  eleq2  2293  ceqsex2  2841  ceqsex6v  2845  vtocl2gaf  2868  ceqsrex2v  2935  mob2  2983  eqreu  2995  nelrdva  3010  dfss4st  3437  undif4  3554  r19.27m  3587  ifbi  3623  preq12bg  3851  opeq2  3858  ralunsn  3876  intab  3952  disjiun  4078  brimralrspcev  4143  opabbid  4149  opthg  4324  pocl  4394  ordelord  4472  ordtriexmid  4613  ontr2exmid  4617  onsucsssucexmid  4619  tfisi  4679  xpeq2  4734  rabxp  4756  vtoclr  4767  opeliunxp  4774  posng  4791  opbrop  4798  rexiunxp  4864  elrnmpt1  4975  dfres2  5057  brcodir  5116  poltletr  5129  xp11m  5167  elxp4  5216  elxp5  5217  dffun4f  5334  fununi  5389  fneq2  5410  fnun  5429  feq3  5458  foeq3  5546  funfveu  5640  funbrfv  5670  ssimaexg  5696  fvopab3g  5707  fvopab3ig  5708  fvelrn  5766  fmptco  5801  fsn2  5809  elunirn  5890  isoeq2  5926  isoeq3  5927  isocnv2  5936  isoini  5942  isopolem  5946  f1oiso  5950  f1oiso2  5951  oprabbid  6057  cbvoprab3  6080  mpomptx  6095  mpofun  6106  ov  6124  ovi3  6142  ov6g  6143  ovg  6144  caoftrn  6251  uchoice  6283  f1o2ndf1  6374  xporderlem  6377  f1od2  6381  brtpos2  6397  brtposg  6400  dftpos4  6409  recseq  6452  tfrlem3-2d  6458  tfrlemi1  6478  tfrexlem  6480  tfr1onlemaccex  6494  tfrcllemaccex  6507  tfrcl  6510  freceq1  6538  freceq2  6539  frecsuc  6553  nnaordex  6674  brecop  6772  eroveu  6773  erovlem  6774  ecopovtrn  6779  ecopovtrng  6782  th3qlem1  6784  th3qlem2  6785  th3q  6787  elpmg  6811  ixpsnval  6848  ixpsnf1o  6883  domeng  6901  dom2lem  6923  xpcomco  6985  xpassen  6989  xpdom2  6990  xpf1o  7005  phplem3g  7017  ssfiexmid  7038  domfiexmid  7040  findcard2  7051  findcard2s  7052  findcard2d  7053  findcard2sd  7054  diffifi  7056  fiintim  7093  opabfi  7100  fidcenumlemrk  7121  fidcenumlemr  7122  supeq2  7156  nninfninc  7290  nnnninfeq2  7296  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  isacnm  7385  acfun  7389  2omotaplemap  7443  2omotaplemst  7444  exmidapne  7446  ccfunen  7450  recexnq  7577  recmulnqg  7578  ltsonq  7585  enq0sym  7619  enq0ref  7620  enq0tr  7621  enq0breq  7623  addnq0mo  7634  mulnq0mo  7635  addnnnq0  7636  mulnnnq0  7637  elinp  7661  prdisj  7679  prarloclem3  7684  prarloc  7690  distrlem5prl  7773  distrlem5pru  7774  ltexprlemell  7785  ltexprlemelu  7786  recexprlemm  7811  addsrmo  7930  mulsrmo  7931  addsrpr  7932  mulsrpr  7933  lttrsr  7949  recexgt0sr  7960  mulgt0sr  7965  ltresr  8026  axprecex  8067  axpre-lttrn  8071  axpre-mulgt0  8074  eqlelt  8233  lesub0  8626  apreap  8734  apreim  8750  aprcl  8793  aptap  8797  zltlen  9525  prime  9546  fzind  9562  qltlen  9835  xltnegi  10031  ixxval  10092  fzval  10206  fzdifsuc  10277  elfzm11  10287  elfzo  10345  zsupcllemex  10450  exbtwnzlemshrink  10468  rebtwn2zlemshrink  10473  facwordi  10962  zfz1iso  11063  pfxsuff1eqwrdeq  11231  wrd2ind  11255  shftfvalg  11329  shftfibg  11331  shftfval  11332  shftfib  11334  shftfn  11335  2shfti  11342  cau3lem  11625  caubnd2  11628  xrmaxiflemcom  11760  clim  11792  clim2  11794  climi  11798  climcn2  11820  addcn2  11821  subcn2  11822  mulcn2  11823  summodclem2a  11892  summodc  11894  fsum3  11898  fsumsplitf  11919  prodfdivap  12058  ntrivcvgap0  12060  prodeq1f  12063  prodeq2w  12067  prodeq2  12068  prodmodc  12089  zproddc  12090  fprodseq  12094  fprodntrivap  12095  fproddivapf  12142  fprodsplitf  12143  fprodsplit1f  12145  sinbnd  12263  cosbnd  12264  divalgb  12436  ndvdssub  12441  gcdval  12480  gcdneg  12503  bezoutlemstep  12518  bezoutlemmain  12519  bezoutlemex  12522  dfgcd2  12535  gcdass  12536  algcvgblem  12571  lcmval  12585  lcmneg  12596  lcmgcdlem  12599  lcmass  12607  qredeq  12618  prmind2  12642  euclemma  12668  pw2dvdslemn  12687  qnumval  12707  qdenval  12708  pceu  12818  pczpre  12820  pcdiv  12825  prmpwdvds  12878  prdsex  13302  gsumpropd  13425  gsumpropd2  13426  gsumress  13428  gsum0g  13429  mnd1  13488  grp1  13639  qusgrp2  13650  nmznsg  13750  releqgg  13757  eqgex  13758  iscmnd  13835  issrg  13928  iscrng2  13978  qusring2  14029  opprunitd  14074  crngunit  14075  dfrhm2  14118  rhmopp  14140  issubrng  14163  resrhm2b  14213  islmod  14255  lsssetm  14320  lsspropdg  14395  ixpsnbasval  14430  basis2  14722  eltg2  14727  isnei  14818  isneip  14820  restbasg  14842  iscnp  14873  iscnp3  14877  tgcn  14882  icnpimaex  14885  lmbrf  14889  cncnp  14904  cnptoprest2  14914  txbas  14932  txcnp  14945  imasnopn  14973  ispsmet  14997  ismet  15018  isxmet  15019  ismet2  15028  blres  15108  metcnp3  15185  txmetcnp  15192  mulcncf  15282  ellimc3apf  15334  limcdifap  15336  limcmpted  15337  limccnp2lem  15350  dvmptfsum  15399  elply2  15409  sincosq3sgn  15502  lgsquadlem1  15756  2sqlem8  15802  2sqlem9  15803  subctctexmid  16366  nnnninfex  16388