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  610  dn1dc  969  dfifp3dc  991  ifpdfbidc  994  xorbi2d  1425  dfbi3dc  1442  xordidc  1444  eleq2w  2296  eleq2  2298  ceqsex2  2857  ceqsex6v  2861  vtocl2gaf  2884  ceqsrex2v  2951  mob2  2999  eqreu  3011  nelrdva  3026  dfss4st  3456  undif4  3573  r19.27m  3607  ifbi  3645  preq12bg  3879  opeq2  3886  ralunsn  3904  intab  3980  disjiun  4106  brimralrspcev  4171  opabbid  4177  opthg  4356  pocl  4426  ordelord  4504  ordtriexmid  4645  ontr2exmid  4649  onsucsssucexmid  4651  tfisi  4711  xpeq2  4766  rabxp  4789  vtoclr  4800  opeliunxp  4807  posng  4824  opbrop  4831  rexiunxp  4899  elrnmpt1  5010  dfres2  5092  brcodir  5152  poltletr  5165  xp11m  5203  elxp4  5252  elxp5  5253  dffun4f  5370  fununi  5426  fneq2  5447  fnun  5466  feq3  5495  foeq3  5590  funfveu  5685  funbrfv  5715  ssimaexg  5741  fvopab3g  5752  fvopab3ig  5753  fvelrn  5810  fmptco  5845  fsn2  5853  elunirn  5941  isoeq2  5977  isoeq3  5978  isocnv2  5987  isoini  5993  isopolem  5997  f1oiso  6001  f1oiso2  6002  oprabbid  6108  cbvoprab3  6131  mpomptx  6146  mpofun  6157  ov  6175  ovi3  6193  ov6g  6194  ovg  6195  caoftrn  6301  uchoice  6333  f1o2ndf1  6426  xporderlem  6429  f1od2  6433  suppimacnvfn  6448  brtpos2  6484  brtposg  6487  dftpos4  6496  recseq  6539  tfrlem3-2d  6545  tfrlemi1  6565  tfrexlem  6567  tfr1onlemaccex  6581  tfrcllemaccex  6594  tfrcl  6597  freceq1  6625  freceq2  6626  frecsuc  6640  nnaordex  6763  brecop  6861  eroveu  6862  erovlem  6863  ecopovtrn  6868  ecopovtrng  6871  th3qlem1  6873  th3qlem2  6874  th3q  6876  elpmg  6900  ixpsnval  6938  ixpsnf1o  6973  domeng  6991  dom2lem  7013  mapsnend  7054  modom  7063  xpcomco  7079  xpassen  7083  xpdom2  7084  xpf1o  7099  phplem3g  7112  ssfiexmid  7133  ssfiexmidt  7135  domfiexmid  7137  findcard2  7148  findcard2s  7149  findcard2d  7150  findcard2sd  7151  diffifi  7153  fiintim  7193  opabfi  7202  fidcenumlemrk  7226  fidcenumlemr  7227  supeq2  7282  nninfninc  7416  nnnninfeq2  7422  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  isacnm  7512  acfun  7516  2omotaplemap  7573  2omotaplemst  7574  exmidapne  7576  ccfunen  7580  recexnq  7707  recmulnqg  7708  ltsonq  7715  enq0sym  7749  enq0ref  7750  enq0tr  7751  enq0breq  7753  addnq0mo  7764  mulnq0mo  7765  addnnnq0  7766  mulnnnq0  7767  elinp  7791  prdisj  7809  prarloclem3  7814  prarloc  7820  distrlem5prl  7903  distrlem5pru  7904  ltexprlemell  7915  ltexprlemelu  7916  recexprlemm  7941  addsrmo  8060  mulsrmo  8061  addsrpr  8062  mulsrpr  8063  lttrsr  8079  recexgt0sr  8090  mulgt0sr  8095  ltresr  8156  axprecex  8197  axpre-lttrn  8201  axpre-mulgt0  8204  eqlelt  8362  lesub0  8755  apreap  8863  apreim  8879  aprcl  8922  aptap  8926  zltlen  9659  prime  9680  fzind  9696  qltlen  9975  xltnegi  10171  ixxval  10232  fzval  10347  fzdifsuc  10419  elfzm11  10429  elfzo  10487  zsupcllemex  10594  exbtwnzlemshrink  10612  rebtwn2zlemshrink  10617  facwordi  11106  zfz1iso  11217  pfxsuff1eqwrdeq  11395  wrd2ind  11419  shftfvalg  11507  shftfibg  11509  shftfval  11510  shftfib  11512  shftfn  11513  2shfti  11520  cau3lem  11803  caubnd2  11806  xrmaxiflemcom  11938  clim  11970  clim2  11972  climi  11976  climcn2  11998  addcn2  11999  subcn2  12000  mulcn2  12001  summodclem2a  12071  summodc  12073  fsum3  12077  fsumsplitf  12098  prodfdivap  12237  ntrivcvgap0  12239  prodeq1f  12242  prodeq2w  12246  prodeq2  12247  prodmodc  12268  zproddc  12269  fprodseq  12273  fprodntrivap  12274  fproddivapf  12321  fprodsplitf  12322  fprodsplit1f  12324  sinbnd  12442  cosbnd  12443  divalgb  12615  ndvdssub  12620  gcdval  12659  gcdneg  12682  bezoutlemstep  12697  bezoutlemmain  12698  bezoutlemex  12701  dfgcd2  12714  gcdass  12715  algcvgblem  12750  lcmval  12764  lcmneg  12775  lcmgcdlem  12778  lcmass  12786  qredeq  12797  prmind2  12821  euclemma  12847  pw2dvdslemn  12866  qnumval  12886  qdenval  12887  pceu  12997  pczpre  12999  pcdiv  13004  prmpwdvds  13057  prdsex  13499  gsumpropd  13622  gsumpropd2  13623  gsumress  13625  gsum0g  13626  mnd1  13685  grp1  13836  qusgrp2  13847  nmznsg  13947  releqgg  13954  eqgex  13955  iscmnd  14032  issrg  14126  iscrng2  14176  qusring2  14227  opprunitd  14272  crngunit  14273  dfrhm2  14316  rhmopp  14338  issubrng  14361  resrhm2b  14411  islmod  14456  lsssetm  14521  lsspropdg  14596  ixpsnbasval  14631  basis2  14930  eltg2  14935  isnei  15026  isneip  15028  restbasg  15050  iscnp  15081  iscnp3  15085  tgcn  15090  icnpimaex  15093  lmbrf  15097  cncnp  15112  cnptoprest2  15122  txbas  15140  txcnp  15153  imasnopn  15181  ispsmet  15205  ismet  15226  isxmet  15227  ismet2  15236  blres  15316  metcnp3  15393  txmetcnp  15400  mulcncf  15490  ellimc3apf  15542  limcdifap  15544  limcmpted  15545  limccnp2lem  15558  dvmptfsum  15607  elply2  15617  sincosq3sgn  15710  pellexlem3  15864  lgsquadlem1  15967  2sqlem8  16013  2sqlem9  16014  eupthres  16469  eupth2lem3lem6fi  16483  subctctexmid  16791  nnnninfex  16817  gfsumval  16879