Theorem anbi2d 460

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 446	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  463  anbi12d  465  bi2anan9  596  dn1dc  945  xorbi2d  1362  dfbi3dc  1379  xordidc  1381  eleq2w  2219  eleq2  2221  ceqsex2  2752  ceqsex6v  2756  vtocl2gaf  2779  ceqsrex2v  2844  mob2  2892  eqreu  2904  nelrdva  2919  dfss4st  3340  undif4  3456  r19.27m  3489  ifbi  3525  preq12bg  3736  opeq2  3742  ralunsn  3760  intab  3836  disjiun  3960  brimralrspcev  4023  opabbid  4029  opthg  4198  pocl  4263  ordelord  4341  ordtriexmid  4480  ontr2exmid  4484  onsucsssucexmid  4486  tfisi  4546  xpeq2  4601  rabxp  4623  vtoclr  4634  opeliunxp  4641  posng  4658  opbrop  4665  rexiunxp  4728  elrnmpt1  4837  dfres2  4918  brcodir  4973  poltletr  4986  xp11m  5024  elxp4  5073  elxp5  5074  dffun4f  5186  fununi  5238  fneq2  5259  fnun  5276  feq3  5304  foeq3  5390  funfveu  5481  funbrfv  5507  ssimaexg  5530  fvopab3g  5541  fvopab3ig  5542  fvelrn  5598  fmptco  5633  fsn2  5641  elunirn  5716  isoeq2  5752  isoeq3  5753  isocnv2  5762  isoini  5768  isopolem  5772  f1oiso  5776  f1oiso2  5777  oprabbid  5874  cbvoprab3  5897  mpomptx  5912  mpofun  5923  ov  5940  ovi3  5957  ov6g  5958  ovg  5959  caoftrn  6057  f1o2ndf1  6175  xporderlem  6178  f1od2  6182  brtpos2  6198  brtposg  6201  dftpos4  6210  recseq  6253  tfrlem3-2d  6259  tfrlemi1  6279  tfrexlem  6281  tfr1onlemaccex  6295  tfrcllemaccex  6308  tfrcl  6311  freceq1  6339  freceq2  6340  frecsuc  6354  nnaordex  6474  brecop  6570  eroveu  6571  erovlem  6572  ecopovtrn  6577  ecopovtrng  6580  th3qlem1  6582  th3qlem2  6583  th3q  6585  elpmg  6609  ixpsnval  6646  ixpsnf1o  6681  domeng  6697  dom2lem  6717  xpcomco  6771  xpassen  6775  xpdom2  6776  xpf1o  6789  phplem3g  6801  ssfiexmid  6821  domfiexmid  6823  findcard2  6834  findcard2s  6835  findcard2d  6836  findcard2sd  6837  diffifi  6839  fiintim  6873  fidcenumlemrk  6898  fidcenumlemr  6899  supeq2  6933  nnnninfeq2  7072  exmidfodomrlemr  7137  exmidfodomrlemrALT  7138  acfun  7142  ccfunen  7184  recexnq  7310  recmulnqg  7311  ltsonq  7318  enq0sym  7352  enq0ref  7353  enq0tr  7354  enq0breq  7356  addnq0mo  7367  mulnq0mo  7368  addnnnq0  7369  mulnnnq0  7370  elinp  7394  prdisj  7412  prarloclem3  7417  prarloc  7423  distrlem5prl  7506  distrlem5pru  7507  ltexprlemell  7518  ltexprlemelu  7519  recexprlemm  7544  addsrmo  7663  mulsrmo  7664  addsrpr  7665  mulsrpr  7666  lttrsr  7682  recexgt0sr  7693  mulgt0sr  7698  ltresr  7759  axprecex  7800  axpre-lttrn  7804  axpre-mulgt0  7807  lesub0  8354  apreap  8462  apreim  8478  aprcl  8521  zltlen  9242  prime  9263  fzind  9279  qltlen  9549  xltnegi  9739  ixxval  9800  fzval  9914  fzdifsuc  9983  elfzm11  9993  elfzo  10048  exbtwnzlemshrink  10148  rebtwn2zlemshrink  10153  facwordi  10614  zfz1iso  10712  shftfvalg  10718  shftfibg  10720  shftfval  10721  shftfib  10723  shftfn  10724  2shfti  10731  cau3lem  11014  caubnd2  11017  xrmaxiflemcom  11146  clim  11178  clim2  11180  climi  11184  climcn2  11206  addcn2  11207  subcn2  11208  mulcn2  11209  summodclem2a  11278  summodc  11280  fsum3  11284  fsumsplitf  11305  prodfdivap  11444  ntrivcvgap0  11446  prodeq1f  11449  prodeq2w  11453  prodeq2  11454  prodmodc  11475  zproddc  11476  fprodseq  11480  fprodntrivap  11481  fproddivapf  11528  fprodsplitf  11529  fprodsplit1f  11531  sinbnd  11649  cosbnd  11650  divalgb  11815  ndvdssub  11820  zsupcllemex  11832  gcdval  11842  gcdneg  11865  bezoutlemstep  11880  bezoutlemmain  11881  bezoutlemex  11884  dfgcd2  11897  gcdass  11898  algcvgblem  11925  lcmval  11939  lcmneg  11950  lcmgcdlem  11953  lcmass  11961  qredeq  11972  prmind2  11996  euclemma  12020  pw2dvdslemn  12039  qnumval  12059  qdenval  12060  basis2  12446  eltg2  12453  isnei  12544  isneip  12546  restbasg  12568  iscnp  12599  iscnp3  12603  tgcn  12608  icnpimaex  12611  lmbrf  12615  cncnp  12630  cnptoprest2  12640  txbas  12658  txcnp  12671  imasnopn  12699  ispsmet  12723  ismet  12744  isxmet  12745  ismet2  12754  blres  12834  metcnp3  12911  txmetcnp  12918  mulcncf  12991  ellimc3apf  13029  limcdifap  13031  limcmpted  13032  limccnp2lem  13045  sincosq3sgn  13149  subctctexmid  13573