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  963  xorbi2d  1400  dfbi3dc  1417  xordidc  1419  eleq2w  2269  eleq2  2271  ceqsex2  2818  ceqsex6v  2822  vtocl2gaf  2845  ceqsrex2v  2912  mob2  2960  eqreu  2972  nelrdva  2987  dfss4st  3414  undif4  3531  r19.27m  3564  ifbi  3600  preq12bg  3827  opeq2  3834  ralunsn  3852  intab  3928  disjiun  4054  brimralrspcev  4119  opabbid  4125  opthg  4300  pocl  4368  ordelord  4446  ordtriexmid  4587  ontr2exmid  4591  onsucsssucexmid  4593  tfisi  4653  xpeq2  4708  rabxp  4730  vtoclr  4741  opeliunxp  4748  posng  4765  opbrop  4772  rexiunxp  4838  elrnmpt1  4948  dfres2  5030  brcodir  5089  poltletr  5102  xp11m  5140  elxp4  5189  elxp5  5190  dffun4f  5306  fununi  5361  fneq2  5382  fnun  5401  feq3  5430  foeq3  5518  funfveu  5612  funbrfv  5640  ssimaexg  5664  fvopab3g  5675  fvopab3ig  5676  fvelrn  5734  fmptco  5769  fsn2  5777  elunirn  5858  isoeq2  5894  isoeq3  5895  isocnv2  5904  isoini  5910  isopolem  5914  f1oiso  5918  f1oiso2  5919  oprabbid  6021  cbvoprab3  6044  mpomptx  6059  mpofun  6070  ov  6088  ovi3  6106  ov6g  6107  ovg  6108  caoftrn  6214  uchoice  6246  f1o2ndf1  6337  xporderlem  6340  f1od2  6344  brtpos2  6360  brtposg  6363  dftpos4  6372  recseq  6415  tfrlem3-2d  6421  tfrlemi1  6441  tfrexlem  6443  tfr1onlemaccex  6457  tfrcllemaccex  6470  tfrcl  6473  freceq1  6501  freceq2  6502  frecsuc  6516  nnaordex  6637  brecop  6735  eroveu  6736  erovlem  6737  ecopovtrn  6742  ecopovtrng  6745  th3qlem1  6747  th3qlem2  6748  th3q  6750  elpmg  6774  ixpsnval  6811  ixpsnf1o  6846  domeng  6864  dom2lem  6886  xpcomco  6946  xpassen  6950  xpdom2  6951  xpf1o  6966  phplem3g  6978  ssfiexmid  6999  domfiexmid  7001  findcard2  7012  findcard2s  7013  findcard2d  7014  findcard2sd  7015  diffifi  7017  fiintim  7054  opabfi  7061  fidcenumlemrk  7082  fidcenumlemr  7083  supeq2  7117  nninfninc  7251  nnnninfeq2  7257  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  isacnm  7346  acfun  7350  2omotaplemap  7404  2omotaplemst  7405  exmidapne  7407  ccfunen  7411  recexnq  7538  recmulnqg  7539  ltsonq  7546  enq0sym  7580  enq0ref  7581  enq0tr  7582  enq0breq  7584  addnq0mo  7595  mulnq0mo  7596  addnnnq0  7597  mulnnnq0  7598  elinp  7622  prdisj  7640  prarloclem3  7645  prarloc  7651  distrlem5prl  7734  distrlem5pru  7735  ltexprlemell  7746  ltexprlemelu  7747  recexprlemm  7772  addsrmo  7891  mulsrmo  7892  addsrpr  7893  mulsrpr  7894  lttrsr  7910  recexgt0sr  7921  mulgt0sr  7926  ltresr  7987  axprecex  8028  axpre-lttrn  8032  axpre-mulgt0  8035  eqlelt  8194  lesub0  8587  apreap  8695  apreim  8711  aprcl  8754  aptap  8758  zltlen  9486  prime  9507  fzind  9523  qltlen  9796  xltnegi  9992  ixxval  10053  fzval  10167  fzdifsuc  10238  elfzm11  10248  elfzo  10306  zsupcllemex  10410  exbtwnzlemshrink  10428  rebtwn2zlemshrink  10433  facwordi  10922  zfz1iso  11023  pfxsuff1eqwrdeq  11190  wrd2ind  11214  shftfvalg  11244  shftfibg  11246  shftfval  11247  shftfib  11249  shftfn  11250  2shfti  11257  cau3lem  11540  caubnd2  11543  xrmaxiflemcom  11675  clim  11707  clim2  11709  climi  11713  climcn2  11735  addcn2  11736  subcn2  11737  mulcn2  11738  summodclem2a  11807  summodc  11809  fsum3  11813  fsumsplitf  11834  prodfdivap  11973  ntrivcvgap0  11975  prodeq1f  11978  prodeq2w  11982  prodeq2  11983  prodmodc  12004  zproddc  12005  fprodseq  12009  fprodntrivap  12010  fproddivapf  12057  fprodsplitf  12058  fprodsplit1f  12060  sinbnd  12178  cosbnd  12179  divalgb  12351  ndvdssub  12356  gcdval  12395  gcdneg  12418  bezoutlemstep  12433  bezoutlemmain  12434  bezoutlemex  12437  dfgcd2  12450  gcdass  12451  algcvgblem  12486  lcmval  12500  lcmneg  12511  lcmgcdlem  12514  lcmass  12522  qredeq  12533  prmind2  12557  euclemma  12583  pw2dvdslemn  12602  qnumval  12622  qdenval  12623  pceu  12733  pczpre  12735  pcdiv  12740  prmpwdvds  12793  prdsex  13216  gsumpropd  13339  gsumpropd2  13340  gsumress  13342  gsum0g  13343  mnd1  13402  grp1  13553  qusgrp2  13564  nmznsg  13664  releqgg  13671  eqgex  13672  iscmnd  13749  issrg  13842  iscrng2  13892  qusring2  13943  opprunitd  13987  crngunit  13988  dfrhm2  14031  rhmopp  14053  issubrng  14076  resrhm2b  14126  islmod  14168  lsssetm  14233  lsspropdg  14308  ixpsnbasval  14343  basis2  14635  eltg2  14640  isnei  14731  isneip  14733  restbasg  14755  iscnp  14786  iscnp3  14790  tgcn  14795  icnpimaex  14798  lmbrf  14802  cncnp  14817  cnptoprest2  14827  txbas  14845  txcnp  14858  imasnopn  14886  ispsmet  14910  ismet  14931  isxmet  14932  ismet2  14941  blres  15021  metcnp3  15098  txmetcnp  15105  mulcncf  15195  ellimc3apf  15247  limcdifap  15249  limcmpted  15250  limccnp2lem  15263  dvmptfsum  15312  elply2  15322  sincosq3sgn  15415  lgsquadlem1  15669  2sqlem8  15715  2sqlem9  15716  subctctexmid  16139  nnnninfex  16161