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  5548  funfveu  5642  funbrfv  5672  ssimaexg  5698  fvopab3g  5709  fvopab3ig  5710  fvelrn  5768  fmptco  5803  fsn2  5811  elunirn  5896  isoeq2  5932  isoeq3  5933  isocnv2  5942  isoini  5948  isopolem  5952  f1oiso  5956  f1oiso2  5957  oprabbid  6063  cbvoprab3  6086  mpomptx  6101  mpofun  6112  ov  6130  ovi3  6148  ov6g  6149  ovg  6150  caoftrn  6257  uchoice  6289  f1o2ndf1  6380  xporderlem  6383  f1od2  6387  brtpos2  6403  brtposg  6406  dftpos4  6415  recseq  6458  tfrlem3-2d  6464  tfrlemi1  6484  tfrexlem  6486  tfr1onlemaccex  6500  tfrcllemaccex  6513  tfrcl  6516  freceq1  6544  freceq2  6545  frecsuc  6559  nnaordex  6682  brecop  6780  eroveu  6781  erovlem  6782  ecopovtrn  6787  ecopovtrng  6790  th3qlem1  6792  th3qlem2  6793  th3q  6795  elpmg  6819  ixpsnval  6856  ixpsnf1o  6891  domeng  6909  dom2lem  6931  xpcomco  6993  xpassen  6997  xpdom2  6998  xpf1o  7013  phplem3g  7025  ssfiexmid  7046  domfiexmid  7048  findcard2  7059  findcard2s  7060  findcard2d  7061  findcard2sd  7062  diffifi  7064  fiintim  7104  opabfi  7111  fidcenumlemrk  7132  fidcenumlemr  7133  supeq2  7167  nninfninc  7301  nnnninfeq2  7307  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  isacnm  7396  acfun  7400  2omotaplemap  7454  2omotaplemst  7455  exmidapne  7457  ccfunen  7461  recexnq  7588  recmulnqg  7589  ltsonq  7596  enq0sym  7630  enq0ref  7631  enq0tr  7632  enq0breq  7634  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  mulnnnq0  7648  elinp  7672  prdisj  7690  prarloclem3  7695  prarloc  7701  distrlem5prl  7784  distrlem5pru  7785  ltexprlemell  7796  ltexprlemelu  7797  recexprlemm  7822  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  lttrsr  7960  recexgt0sr  7971  mulgt0sr  7976  ltresr  8037  axprecex  8078  axpre-lttrn  8082  axpre-mulgt0  8085  eqlelt  8244  lesub0  8637  apreap  8745  apreim  8761  aprcl  8804  aptap  8808  zltlen  9536  prime  9557  fzind  9573  qltlen  9847  xltnegi  10043  ixxval  10104  fzval  10218  fzdifsuc  10289  elfzm11  10299  elfzo  10357  zsupcllemex  10462  exbtwnzlemshrink  10480  rebtwn2zlemshrink  10485  facwordi  10974  zfz1iso  11076  pfxsuff1eqwrdeq  11247  wrd2ind  11271  shftfvalg  11345  shftfibg  11347  shftfval  11348  shftfib  11350  shftfn  11351  2shfti  11358  cau3lem  11641  caubnd2  11644  xrmaxiflemcom  11776  clim  11808  clim2  11810  climi  11814  climcn2  11836  addcn2  11837  subcn2  11838  mulcn2  11839  summodclem2a  11908  summodc  11910  fsum3  11914  fsumsplitf  11935  prodfdivap  12074  ntrivcvgap0  12076  prodeq1f  12079  prodeq2w  12083  prodeq2  12084  prodmodc  12105  zproddc  12106  fprodseq  12110  fprodntrivap  12111  fproddivapf  12158  fprodsplitf  12159  fprodsplit1f  12161  sinbnd  12279  cosbnd  12280  divalgb  12452  ndvdssub  12457  gcdval  12496  gcdneg  12519  bezoutlemstep  12534  bezoutlemmain  12535  bezoutlemex  12538  dfgcd2  12551  gcdass  12552  algcvgblem  12587  lcmval  12601  lcmneg  12612  lcmgcdlem  12615  lcmass  12623  qredeq  12634  prmind2  12658  euclemma  12684  pw2dvdslemn  12703  qnumval  12723  qdenval  12724  pceu  12834  pczpre  12836  pcdiv  12841  prmpwdvds  12894  prdsex  13318  gsumpropd  13441  gsumpropd2  13442  gsumress  13444  gsum0g  13445  mnd1  13504  grp1  13655  qusgrp2  13666  nmznsg  13766  releqgg  13773  eqgex  13774  iscmnd  13851  issrg  13944  iscrng2  13994  qusring2  14045  opprunitd  14090  crngunit  14091  dfrhm2  14134  rhmopp  14156  issubrng  14179  resrhm2b  14229  islmod  14271  lsssetm  14336  lsspropdg  14411  ixpsnbasval  14446  basis2  14738  eltg2  14743  isnei  14834  isneip  14836  restbasg  14858  iscnp  14889  iscnp3  14893  tgcn  14898  icnpimaex  14901  lmbrf  14905  cncnp  14920  cnptoprest2  14930  txbas  14948  txcnp  14961  imasnopn  14989  ispsmet  15013  ismet  15034  isxmet  15035  ismet2  15044  blres  15124  metcnp3  15201  txmetcnp  15208  mulcncf  15298  ellimc3apf  15350  limcdifap  15352  limcmpted  15353  limccnp2lem  15366  dvmptfsum  15415  elply2  15425  sincosq3sgn  15518  lgsquadlem1  15772  2sqlem8  15818  2sqlem9  15819  subctctexmid  16453  nnnninfex  16476