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  2267  eleq2  2269  ceqsex2  2813  ceqsex6v  2817  vtocl2gaf  2840  ceqsrex2v  2905  mob2  2953  eqreu  2965  nelrdva  2980  dfss4st  3406  undif4  3523  r19.27m  3556  ifbi  3591  preq12bg  3814  opeq2  3820  ralunsn  3838  intab  3914  disjiun  4039  brimralrspcev  4103  opabbid  4109  opthg  4282  pocl  4350  ordelord  4428  ordtriexmid  4569  ontr2exmid  4573  onsucsssucexmid  4575  tfisi  4635  xpeq2  4690  rabxp  4712  vtoclr  4723  opeliunxp  4730  posng  4747  opbrop  4754  rexiunxp  4820  elrnmpt1  4929  dfres2  5011  brcodir  5070  poltletr  5083  xp11m  5121  elxp4  5170  elxp5  5171  dffun4f  5287  fununi  5342  fneq2  5363  fnun  5382  feq3  5410  foeq3  5496  funfveu  5589  funbrfv  5617  ssimaexg  5641  fvopab3g  5652  fvopab3ig  5653  fvelrn  5711  fmptco  5746  fsn2  5754  elunirn  5835  isoeq2  5871  isoeq3  5872  isocnv2  5881  isoini  5887  isopolem  5891  f1oiso  5895  f1oiso2  5896  oprabbid  5998  cbvoprab3  6021  mpomptx  6036  mpofun  6047  ov  6065  ovi3  6083  ov6g  6084  ovg  6085  caoftrn  6191  uchoice  6223  f1o2ndf1  6314  xporderlem  6317  f1od2  6321  brtpos2  6337  brtposg  6340  dftpos4  6349  recseq  6392  tfrlem3-2d  6398  tfrlemi1  6418  tfrexlem  6420  tfr1onlemaccex  6434  tfrcllemaccex  6447  tfrcl  6450  freceq1  6478  freceq2  6479  frecsuc  6493  nnaordex  6614  brecop  6712  eroveu  6713  erovlem  6714  ecopovtrn  6719  ecopovtrng  6722  th3qlem1  6724  th3qlem2  6725  th3q  6727  elpmg  6751  ixpsnval  6788  ixpsnf1o  6823  domeng  6841  dom2lem  6863  xpcomco  6921  xpassen  6925  xpdom2  6926  xpf1o  6941  phplem3g  6953  ssfiexmid  6973  domfiexmid  6975  findcard2  6986  findcard2s  6987  findcard2d  6988  findcard2sd  6989  diffifi  6991  fiintim  7028  opabfi  7035  fidcenumlemrk  7056  fidcenumlemr  7057  supeq2  7091  nninfninc  7225  nnnninfeq2  7231  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  isacnm  7315  acfun  7319  2omotaplemap  7369  2omotaplemst  7370  exmidapne  7372  ccfunen  7376  recexnq  7503  recmulnqg  7504  ltsonq  7511  enq0sym  7545  enq0ref  7546  enq0tr  7547  enq0breq  7549  addnq0mo  7560  mulnq0mo  7561  addnnnq0  7562  mulnnnq0  7563  elinp  7587  prdisj  7605  prarloclem3  7610  prarloc  7616  distrlem5prl  7699  distrlem5pru  7700  ltexprlemell  7711  ltexprlemelu  7712  recexprlemm  7737  addsrmo  7856  mulsrmo  7857  addsrpr  7858  mulsrpr  7859  lttrsr  7875  recexgt0sr  7886  mulgt0sr  7891  ltresr  7952  axprecex  7993  axpre-lttrn  7997  axpre-mulgt0  8000  eqlelt  8159  lesub0  8552  apreap  8660  apreim  8676  aprcl  8719  aptap  8723  zltlen  9451  prime  9472  fzind  9488  qltlen  9761  xltnegi  9957  ixxval  10018  fzval  10132  fzdifsuc  10203  elfzm11  10213  elfzo  10271  zsupcllemex  10373  exbtwnzlemshrink  10391  rebtwn2zlemshrink  10396  facwordi  10885  zfz1iso  10986  shftfvalg  11129  shftfibg  11131  shftfval  11132  shftfib  11134  shftfn  11135  2shfti  11142  cau3lem  11425  caubnd2  11428  xrmaxiflemcom  11560  clim  11592  clim2  11594  climi  11598  climcn2  11620  addcn2  11621  subcn2  11622  mulcn2  11623  summodclem2a  11692  summodc  11694  fsum3  11698  fsumsplitf  11719  prodfdivap  11858  ntrivcvgap0  11860  prodeq1f  11863  prodeq2w  11867  prodeq2  11868  prodmodc  11889  zproddc  11890  fprodseq  11894  fprodntrivap  11895  fproddivapf  11942  fprodsplitf  11943  fprodsplit1f  11945  sinbnd  12063  cosbnd  12064  divalgb  12236  ndvdssub  12241  gcdval  12280  gcdneg  12303  bezoutlemstep  12318  bezoutlemmain  12319  bezoutlemex  12322  dfgcd2  12335  gcdass  12336  algcvgblem  12371  lcmval  12385  lcmneg  12396  lcmgcdlem  12399  lcmass  12407  qredeq  12418  prmind2  12442  euclemma  12468  pw2dvdslemn  12487  qnumval  12507  qdenval  12508  pceu  12618  pczpre  12620  pcdiv  12625  prmpwdvds  12678  prdsex  13101  gsumpropd  13224  gsumpropd2  13225  gsumress  13227  gsum0g  13228  mnd1  13287  grp1  13438  qusgrp2  13449  nmznsg  13549  releqgg  13556  eqgex  13557  iscmnd  13634  issrg  13727  iscrng2  13777  qusring2  13828  opprunitd  13872  crngunit  13873  dfrhm2  13916  rhmopp  13938  issubrng  13961  resrhm2b  14011  islmod  14053  lsssetm  14118  lsspropdg  14193  ixpsnbasval  14228  basis2  14520  eltg2  14525  isnei  14616  isneip  14618  restbasg  14640  iscnp  14671  iscnp3  14675  tgcn  14680  icnpimaex  14683  lmbrf  14687  cncnp  14702  cnptoprest2  14712  txbas  14730  txcnp  14743  imasnopn  14771  ispsmet  14795  ismet  14816  isxmet  14817  ismet2  14826  blres  14906  metcnp3  14983  txmetcnp  14990  mulcncf  15080  ellimc3apf  15132  limcdifap  15134  limcmpted  15135  limccnp2lem  15148  dvmptfsum  15197  elply2  15207  sincosq3sgn  15300  lgsquadlem1  15554  2sqlem8  15600  2sqlem9  15601  subctctexmid  15937  nnnninfex  15959