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  2255  eleq2  2257  ceqsex2  2800  ceqsex6v  2804  vtocl2gaf  2827  ceqsrex2v  2892  mob2  2940  eqreu  2952  nelrdva  2967  dfss4st  3392  undif4  3509  r19.27m  3542  ifbi  3577  preq12bg  3799  opeq2  3805  ralunsn  3823  intab  3899  disjiun  4024  brimralrspcev  4088  opabbid  4094  opthg  4267  pocl  4334  ordelord  4412  ordtriexmid  4553  ontr2exmid  4557  onsucsssucexmid  4559  tfisi  4619  xpeq2  4674  rabxp  4696  vtoclr  4707  opeliunxp  4714  posng  4731  opbrop  4738  rexiunxp  4804  elrnmpt1  4913  dfres2  4994  brcodir  5053  poltletr  5066  xp11m  5104  elxp4  5153  elxp5  5154  dffun4f  5270  fununi  5322  fneq2  5343  fnun  5360  feq3  5388  foeq3  5474  funfveu  5567  funbrfv  5595  ssimaexg  5619  fvopab3g  5630  fvopab3ig  5631  fvelrn  5689  fmptco  5724  fsn2  5732  elunirn  5809  isoeq2  5845  isoeq3  5846  isocnv2  5855  isoini  5861  isopolem  5865  f1oiso  5869  f1oiso2  5870  oprabbid  5971  cbvoprab3  5994  mpomptx  6009  mpofun  6020  ov  6038  ovi3  6055  ov6g  6056  ovg  6057  caoftrn  6158  uchoice  6190  f1o2ndf1  6281  xporderlem  6284  f1od2  6288  brtpos2  6304  brtposg  6307  dftpos4  6316  recseq  6359  tfrlem3-2d  6365  tfrlemi1  6385  tfrexlem  6387  tfr1onlemaccex  6401  tfrcllemaccex  6414  tfrcl  6417  freceq1  6445  freceq2  6446  frecsuc  6460  nnaordex  6581  brecop  6679  eroveu  6680  erovlem  6681  ecopovtrn  6686  ecopovtrng  6689  th3qlem1  6691  th3qlem2  6692  th3q  6694  elpmg  6718  ixpsnval  6755  ixpsnf1o  6790  domeng  6806  dom2lem  6826  xpcomco  6880  xpassen  6884  xpdom2  6885  xpf1o  6900  phplem3g  6912  ssfiexmid  6932  domfiexmid  6934  findcard2  6945  findcard2s  6946  findcard2d  6947  findcard2sd  6948  diffifi  6950  fiintim  6985  opabfi  6992  fidcenumlemrk  7013  fidcenumlemr  7014  supeq2  7048  nninfninc  7182  nnnninfeq2  7188  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  acfun  7267  2omotaplemap  7317  2omotaplemst  7318  exmidapne  7320  ccfunen  7324  recexnq  7450  recmulnqg  7451  ltsonq  7458  enq0sym  7492  enq0ref  7493  enq0tr  7494  enq0breq  7496  addnq0mo  7507  mulnq0mo  7508  addnnnq0  7509  mulnnnq0  7510  elinp  7534  prdisj  7552  prarloclem3  7557  prarloc  7563  distrlem5prl  7646  distrlem5pru  7647  ltexprlemell  7658  ltexprlemelu  7659  recexprlemm  7684  addsrmo  7803  mulsrmo  7804  addsrpr  7805  mulsrpr  7806  lttrsr  7822  recexgt0sr  7833  mulgt0sr  7838  ltresr  7899  axprecex  7940  axpre-lttrn  7944  axpre-mulgt0  7947  eqlelt  8106  lesub0  8498  apreap  8606  apreim  8622  aprcl  8665  aptap  8669  zltlen  9395  prime  9416  fzind  9432  qltlen  9705  xltnegi  9901  ixxval  9962  fzval  10076  fzdifsuc  10147  elfzm11  10157  elfzo  10215  exbtwnzlemshrink  10317  rebtwn2zlemshrink  10322  facwordi  10811  zfz1iso  10912  shftfvalg  10962  shftfibg  10964  shftfval  10965  shftfib  10967  shftfn  10968  2shfti  10975  cau3lem  11258  caubnd2  11261  xrmaxiflemcom  11392  clim  11424  clim2  11426  climi  11430  climcn2  11452  addcn2  11453  subcn2  11454  mulcn2  11455  summodclem2a  11524  summodc  11526  fsum3  11530  fsumsplitf  11551  prodfdivap  11690  ntrivcvgap0  11692  prodeq1f  11695  prodeq2w  11699  prodeq2  11700  prodmodc  11721  zproddc  11722  fprodseq  11726  fprodntrivap  11727  fproddivapf  11774  fprodsplitf  11775  fprodsplit1f  11777  sinbnd  11895  cosbnd  11896  divalgb  12066  ndvdssub  12071  zsupcllemex  12083  gcdval  12096  gcdneg  12119  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlemex  12138  dfgcd2  12151  gcdass  12152  algcvgblem  12187  lcmval  12201  lcmneg  12212  lcmgcdlem  12215  lcmass  12223  qredeq  12234  prmind2  12258  euclemma  12284  pw2dvdslemn  12303  qnumval  12323  qdenval  12324  pceu  12433  pczpre  12435  pcdiv  12440  prmpwdvds  12493  prdsex  12880  gsumpropd  12975  gsumpropd2  12976  gsumress  12978  gsum0g  12979  mnd1  13027  grp1  13178  qusgrp2  13183  nmznsg  13283  releqgg  13290  eqgex  13291  iscmnd  13368  issrg  13461  iscrng2  13511  qusring2  13562  opprunitd  13606  crngunit  13607  dfrhm2  13650  rhmopp  13672  issubrng  13695  resrhm2b  13745  islmod  13787  lsssetm  13852  lsspropdg  13927  ixpsnbasval  13962  basis2  14216  eltg2  14221  isnei  14312  isneip  14314  restbasg  14336  iscnp  14367  iscnp3  14371  tgcn  14376  icnpimaex  14379  lmbrf  14383  cncnp  14398  cnptoprest2  14408  txbas  14426  txcnp  14439  imasnopn  14467  ispsmet  14491  ismet  14512  isxmet  14513  ismet2  14522  blres  14602  metcnp3  14679  txmetcnp  14686  mulcncf  14762  ellimc3apf  14814  limcdifap  14816  limcmpted  14817  limccnp2lem  14830  elply2  14881  sincosq3sgn  14963  lgsquadlem1  15191  2sqlem8  15210  2sqlem9  15211  subctctexmid  15491