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  4325  pocl  4395  ordelord  4473  ordtriexmid  4614  ontr2exmid  4618  onsucsssucexmid  4620  tfisi  4680  xpeq2  4735  rabxp  4758  vtoclr  4769  opeliunxp  4776  posng  4793  opbrop  4800  rexiunxp  4867  elrnmpt1  4978  dfres2  5060  brcodir  5119  poltletr  5132  xp11m  5170  elxp4  5219  elxp5  5220  dffun4f  5337  fununi  5392  fneq2  5413  fnun  5432  feq3  5461  foeq3  5551  funfveu  5645  funbrfv  5675  ssimaexg  5701  fvopab3g  5712  fvopab3ig  5713  fvelrn  5771  fmptco  5806  fsn2  5814  elunirn  5899  isoeq2  5935  isoeq3  5936  isocnv2  5945  isoini  5951  isopolem  5955  f1oiso  5959  f1oiso2  5960  oprabbid  6066  cbvoprab3  6089  mpomptx  6104  mpofun  6115  ov  6133  ovi3  6151  ov6g  6152  ovg  6153  caoftrn  6260  uchoice  6292  f1o2ndf1  6385  xporderlem  6388  f1od2  6392  brtpos2  6408  brtposg  6411  dftpos4  6420  recseq  6463  tfrlem3-2d  6469  tfrlemi1  6489  tfrexlem  6491  tfr1onlemaccex  6505  tfrcllemaccex  6518  tfrcl  6521  freceq1  6549  freceq2  6550  frecsuc  6564  nnaordex  6687  brecop  6785  eroveu  6786  erovlem  6787  ecopovtrn  6792  ecopovtrng  6795  th3qlem1  6797  th3qlem2  6798  th3q  6800  elpmg  6824  ixpsnval  6861  ixpsnf1o  6896  domeng  6914  dom2lem  6936  xpcomco  6998  xpassen  7002  xpdom2  7003  xpf1o  7018  phplem3g  7030  ssfiexmid  7051  domfiexmid  7053  findcard2  7064  findcard2s  7065  findcard2d  7066  findcard2sd  7067  diffifi  7069  fiintim  7109  opabfi  7116  fidcenumlemrk  7137  fidcenumlemr  7138  supeq2  7172  nninfninc  7306  nnnninfeq2  7312  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  isacnm  7401  acfun  7405  2omotaplemap  7459  2omotaplemst  7460  exmidapne  7462  ccfunen  7466  recexnq  7593  recmulnqg  7594  ltsonq  7601  enq0sym  7635  enq0ref  7636  enq0tr  7637  enq0breq  7639  addnq0mo  7650  mulnq0mo  7651  addnnnq0  7652  mulnnnq0  7653  elinp  7677  prdisj  7695  prarloclem3  7700  prarloc  7706  distrlem5prl  7789  distrlem5pru  7790  ltexprlemell  7801  ltexprlemelu  7802  recexprlemm  7827  addsrmo  7946  mulsrmo  7947  addsrpr  7948  mulsrpr  7949  lttrsr  7965  recexgt0sr  7976  mulgt0sr  7981  ltresr  8042  axprecex  8083  axpre-lttrn  8087  axpre-mulgt0  8090  eqlelt  8249  lesub0  8642  apreap  8750  apreim  8766  aprcl  8809  aptap  8813  zltlen  9541  prime  9562  fzind  9578  qltlen  9852  xltnegi  10048  ixxval  10109  fzval  10223  fzdifsuc  10294  elfzm11  10304  elfzo  10362  zsupcllemex  10467  exbtwnzlemshrink  10485  rebtwn2zlemshrink  10490  facwordi  10979  zfz1iso  11081  pfxsuff1eqwrdeq  11252  wrd2ind  11276  shftfvalg  11350  shftfibg  11352  shftfval  11353  shftfib  11355  shftfn  11356  2shfti  11363  cau3lem  11646  caubnd2  11649  xrmaxiflemcom  11781  clim  11813  clim2  11815  climi  11819  climcn2  11841  addcn2  11842  subcn2  11843  mulcn2  11844  summodclem2a  11913  summodc  11915  fsum3  11919  fsumsplitf  11940  prodfdivap  12079  ntrivcvgap0  12081  prodeq1f  12084  prodeq2w  12088  prodeq2  12089  prodmodc  12110  zproddc  12111  fprodseq  12115  fprodntrivap  12116  fproddivapf  12163  fprodsplitf  12164  fprodsplit1f  12166  sinbnd  12284  cosbnd  12285  divalgb  12457  ndvdssub  12462  gcdval  12501  gcdneg  12524  bezoutlemstep  12539  bezoutlemmain  12540  bezoutlemex  12543  dfgcd2  12556  gcdass  12557  algcvgblem  12592  lcmval  12606  lcmneg  12617  lcmgcdlem  12620  lcmass  12628  qredeq  12639  prmind2  12663  euclemma  12689  pw2dvdslemn  12708  qnumval  12728  qdenval  12729  pceu  12839  pczpre  12841  pcdiv  12846  prmpwdvds  12899  prdsex  13323  gsumpropd  13446  gsumpropd2  13447  gsumress  13449  gsum0g  13450  mnd1  13509  grp1  13660  qusgrp2  13671  nmznsg  13771  releqgg  13778  eqgex  13779  iscmnd  13856  issrg  13949  iscrng2  13999  qusring2  14050  opprunitd  14095  crngunit  14096  dfrhm2  14139  rhmopp  14161  issubrng  14184  resrhm2b  14234  islmod  14276  lsssetm  14341  lsspropdg  14416  ixpsnbasval  14451  basis2  14743  eltg2  14748  isnei  14839  isneip  14841  restbasg  14863  iscnp  14894  iscnp3  14898  tgcn  14903  icnpimaex  14906  lmbrf  14910  cncnp  14925  cnptoprest2  14935  txbas  14953  txcnp  14966  imasnopn  14994  ispsmet  15018  ismet  15039  isxmet  15040  ismet2  15049  blres  15129  metcnp3  15206  txmetcnp  15213  mulcncf  15303  ellimc3apf  15355  limcdifap  15357  limcmpted  15358  limccnp2lem  15371  dvmptfsum  15420  elply2  15430  sincosq3sgn  15523  lgsquadlem1  15777  2sqlem8  15823  2sqlem9  15824  subctctexmid  16479  nnnninfex  16502