Theorem anbi2d 459

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 445	1 |- ( ph -> ( ( th /\ ps ) <-> ( th /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anbi2  462  anbi12d  464  bi2anan9  595  dn1dc  944  xorbi2d  1358  dfbi3dc  1375  xordidc  1377  eleq2w  2199  eleq2  2201  ceqsex2  2721  ceqsex6v  2725  vtocl2gaf  2748  ceqsrex2v  2812  mob2  2859  eqreu  2871  nelrdva  2886  dfss4st  3304  undif4  3420  r19.27m  3453  ifbi  3487  preq12bg  3695  opeq2  3701  ralunsn  3719  intab  3795  disjiun  3919  brimralrspcev  3982  opabbid  3988  opthg  4155  pocl  4220  ordelord  4298  ordtriexmid  4432  ontr2exmid  4435  onsucsssucexmid  4437  tfisi  4496  xpeq2  4549  rabxp  4571  vtoclr  4582  opeliunxp  4589  posng  4606  opbrop  4613  rexiunxp  4676  elrnmpt1  4785  dfres2  4866  brcodir  4921  poltletr  4934  xp11m  4972  elxp4  5021  elxp5  5022  dffun4f  5134  fununi  5186  fneq2  5207  fnun  5224  feq3  5252  foeq3  5338  funfveu  5427  funbrfv  5453  ssimaexg  5476  fvopab3g  5487  fvopab3ig  5488  fvelrn  5544  fmptco  5579  fsn2  5587  elunirn  5660  isoeq2  5696  isoeq3  5697  isocnv2  5706  isoini  5712  isopolem  5716  f1oiso  5720  f1oiso2  5721  oprabbid  5817  cbvoprab3  5840  mpomptx  5855  mpofun  5866  ov  5883  ovi3  5900  ov6g  5901  ovg  5902  caoftrn  6000  f1o2ndf1  6118  xporderlem  6121  f1od2  6125  brtpos2  6141  brtposg  6144  dftpos4  6153  recseq  6196  tfrlem3-2d  6202  tfrlemi1  6222  tfrexlem  6224  tfr1onlemaccex  6238  tfrcllemaccex  6251  tfrcl  6254  freceq1  6282  freceq2  6283  frecsuc  6297  nnaordex  6416  brecop  6512  eroveu  6513  erovlem  6514  ecopovtrn  6519  ecopovtrng  6522  th3qlem1  6524  th3qlem2  6525  th3q  6527  elpmg  6551  ixpsnval  6588  ixpsnf1o  6623  domeng  6639  dom2lem  6659  xpcomco  6713  xpassen  6717  xpdom2  6718  xpf1o  6731  phplem3g  6743  ssfiexmid  6763  domfiexmid  6765  findcard2  6776  findcard2s  6777  findcard2d  6778  findcard2sd  6779  diffifi  6781  fiintim  6810  fidcenumlemrk  6835  fidcenumlemr  6836  supeq2  6869  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  acfun  7056  ccfunen  7072  recexnq  7191  recmulnqg  7192  ltsonq  7199  enq0sym  7233  enq0ref  7234  enq0tr  7235  enq0breq  7237  addnq0mo  7248  mulnq0mo  7249  addnnnq0  7250  mulnnnq0  7251  elinp  7275  prdisj  7293  prarloclem3  7298  prarloc  7304  distrlem5prl  7387  distrlem5pru  7388  ltexprlemell  7399  ltexprlemelu  7400  recexprlemm  7425  addsrmo  7544  mulsrmo  7545  addsrpr  7546  mulsrpr  7547  lttrsr  7563  recexgt0sr  7574  mulgt0sr  7579  ltresr  7640  axprecex  7681  axpre-lttrn  7685  axpre-mulgt0  7688  lesub0  8234  apreap  8342  apreim  8358  aprcl  8401  zltlen  9122  prime  9143  fzind  9159  qltlen  9425  xltnegi  9611  ixxval  9672  fzval  9785  fzdifsuc  9854  elfzm11  9864  elfzo  9919  exbtwnzlemshrink  10019  rebtwn2zlemshrink  10024  facwordi  10479  zfz1iso  10577  shftfvalg  10583  shftfibg  10585  shftfval  10586  shftfib  10588  shftfn  10589  2shfti  10596  cau3lem  10879  caubnd2  10882  xrmaxiflemcom  11011  clim  11043  clim2  11045  climi  11049  climcn2  11071  addcn2  11072  subcn2  11073  mulcn2  11074  summodclem2a  11143  summodc  11145  fsum3  11149  fsumsplitf  11170  prodfdivap  11309  ntrivcvgap0  11311  prodeq1f  11314  prodeq2w  11318  prodeq2  11319  sinbnd  11448  cosbnd  11449  divalgb  11611  ndvdssub  11616  zsupcllemex  11628  gcdval  11637  gcdneg  11659  bezoutlemstep  11674  bezoutlemmain  11675  bezoutlemex  11678  dfgcd2  11691  gcdass  11692  algcvgblem  11719  lcmval  11733  lcmneg  11744  lcmgcdlem  11747  lcmass  11755  qredeq  11766  prmind2  11790  euclemma  11813  pw2dvdslemn  11832  qnumval  11852  qdenval  11853  basis2  12204  eltg2  12211  isnei  12302  isneip  12304  restbasg  12326  iscnp  12357  iscnp3  12361  tgcn  12366  icnpimaex  12369  lmbrf  12373  cncnp  12388  cnptoprest2  12398  txbas  12416  txcnp  12429  imasnopn  12457  ispsmet  12481  ismet  12502  isxmet  12503  ismet2  12512  blres  12592  metcnp3  12669  txmetcnp  12676  mulcncf  12749  ellimc3apf  12787  limcdifap  12789  limcmpted  12790  limccnp2lem  12803  sincosq3sgn  12898  subctctexmid  13185