Theorem anbi2d 468

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 454	1 |- ( ph -> ( ( th /\ ps ) <-> ( th /\ ch ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anbi2  471  anbi1cd  472  anbi12d  477  bi2anan9  614  dn1dc  973  dfifp3dc  995  ifpdfbidc  998  xorbi2d  1429  dfbi3dc  1446  xordidc  1448  eleq2w  2300  eleq2  2302  ceqsex2  2863  ceqsex6v  2867  vtocl2gaf  2890  ceqsrex2v  2958  mob2  3006  eqreu  3018  nelrdva  3033  dfss4st  3464  undif4  3587  r19.27m  3623  ifbi  3661  preq12bg  3898  opeq2  3905  ralunsn  3923  intab  3999  disjiun  4125  brimralrspcev  4190  opabbid  4196  opthg  4378  pocl  4448  ordelord  4526  ordtriexmid  4668  ontr2exmid  4672  onsucsssucexmid  4674  tfisi  4734  xpeq2  4789  rabxp  4812  vtoclr  4823  opeliunxp  4830  posng  4847  opbrop  4854  rexiunxp  4922  elrnmpt1  5033  dfres2  5115  brcodir  5175  poltletr  5188  xp11m  5226  elxp4  5275  elxp5  5276  dffun4f  5393  fununi  5449  fneq2  5470  fnun  5489  feq3  5518  foeq3  5613  funfveu  5708  funbrfv  5739  ssimaexg  5765  fvopab3g  5778  fvopab3ig  5779  fvelrn  5839  fmptco  5874  fsn2  5882  elunirn  5972  isoeq2  6008  isoeq3  6009  isocnv2  6018  isoini  6024  isopolem  6028  f1oiso  6032  f1oiso2  6033  oprabbid  6141  cbvoprab3  6164  mpomptx  6179  mpofun  6190  ov  6208  ovi3  6226  ov6g  6227  ovg  6228  caoftrn  6335  uchoice  6371  f1o2ndf1  6464  xporderlem  6467  f1od2  6471  suppimacnvfn  6486  brtpos2  6522  brtposg  6525  dftpos4  6534  recseq  6577  tfrlem3-2d  6583  tfrlemi1  6603  tfrexlem  6605  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfrcl  6635  freceq1  6663  freceq2  6664  frecsuc  6678  nnaordex  6801  brecop  6899  eroveu  6900  erovlem  6901  ecopovtrn  6906  ecopovtrng  6909  th3qlem1  6911  th3qlem2  6912  th3q  6914  elpmg  6938  ixpsnval  6983  ixpsnf1o  7018  domeng  7036  dom2lem  7058  mapsnend  7099  modom  7108  xpcomco  7124  xpassen  7128  xpdom2  7129  xpf1o  7144  phplem3g  7157  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  findcard2  7193  findcard2s  7194  findcard2d  7195  findcard2sd  7196  diffifi  7198  fiintim  7238  opabfi  7247  fidcenumlemrk  7271  fidcenumlemr  7272  supeq2  7330  nninfninc  7464  nnnninfeq2  7470  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  isacnm  7560  acfun  7564  2omotaplemap  7624  2omotaplemst  7625  exmidapne  7627  ccfunen  7631  recexnq  7758  recmulnqg  7759  ltsonq  7766  enq0sym  7800  enq0ref  7801  enq0tr  7802  enq0breq  7804  addnq0mo  7815  mulnq0mo  7816  addnnnq0  7817  mulnnnq0  7818  elinp  7842  prdisj  7860  prarloclem3  7865  prarloc  7871  distrlem5prl  7954  distrlem5pru  7955  ltexprlemell  7966  ltexprlemelu  7967  recexprlemm  7992  addsrmo  8111  mulsrmo  8112  addsrpr  8113  mulsrpr  8114  lttrsr  8130  recexgt0sr  8141  mulgt0sr  8146  ltresr  8207  axprecex  8248  axpre-lttrn  8252  axpre-mulgt0  8255  eqlelt  8413  lesub0  8809  apreap  8918  apreim  8934  aprcl  8977  aptap  8981  zltlen  9729  prime  9750  fzind  9766  qltlen  10050  xltnegi  10248  ixxval  10309  fzval  10424  fzdifsuc  10499  elfzm11  10509  elfzo  10567  zsupcllemex  10674  exbtwnzlemshrink  10694  rebtwn2zlemshrink  10699  facwordi  11194  zfz1iso  11309  pfxsuff1eqwrdeq  11487  wrd2ind  11511  shftfvalg  11599  shftfibg  11601  shftfval  11602  shftfib  11604  shftfn  11605  2shfti  11612  cau3lem  11897  caubnd2  11900  xrmaxiflemcom  12034  clim  12066  clim2  12068  climi  12072  climcn2  12094  addcn2  12095  subcn2  12096  mulcn2  12097  summodclem2a  12167  summodc  12169  fsum3  12173  fsumsplitf  12194  prodfdivap  12333  ntrivcvgap0  12335  prodeq1f  12338  prodeq2w  12342  prodeq2  12343  prodmodc  12364  zproddc  12365  fprodseq  12369  fprodntrivap  12370  fproddivapf  12417  fprodsplitf  12418  fprodsplit1f  12420  sinbnd  12538  cosbnd  12539  divalgb  12711  ndvdssub  12716  gcdval  12755  gcdneg  12778  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlemex  12797  dfgcd2  12810  gcdass  12811  algcvgblem  12846  lcmval  12860  lcmneg  12871  lcmgcdlem  12874  lcmass  12882  qredeq  12893  prmind2  12917  euclemma  12944  pwbdvdslemn  12963  qnumval  12984  qdenval  12985  pceu  13097  pczpre  13099  pcdiv  13104  prmpwdvds  13157  gzsumress  13765  gzsum0  13766  mnd1  13815  grp1  13964  qusgrp2  13969  nmznsg  14069  releqgg  14076  eqgex  14077  resscntz  14160  iscmnd  14185  gsumvalfi  14236  prdsex  14256  issrg  14353  iscrng2  14403  qusring2  14455  opprunitd  14501  crngunit  14502  dfrhm2  14545  rhmopp  14567  issubrng  14591  resrhm2b  14641  islmod  14711  lsssetm  14777  lsspropdg  14852  ixpsnbasval  14887  basis2  15240  eltg2  15245  isnei  15336  isneip  15338  restbasg  15360  iscnp  15391  iscnp3  15395  tgcn  15400  icnpimaex  15403  lmbrf  15407  cncnp  15422  cnptoprest2  15432  txbas  15450  txcnp  15463  imasnopn  15491  ispsmet  15515  ismet  15536  isxmet  15537  ismet2  15546  blres  15626  metcnp3  15703  txmetcnp  15710  mulcncf  15800  ellimc3apf  15852  limcdifap  15854  limcmpted  15855  limccnp2lem  15868  dvmptfsum  15917  elply2  15927  sincosq3sgn  16021  zprmlogbaplem3  16178  pellexlem3  16192  lgsquadlem1  16362  2sqlem8  16408  2sqlem9  16409  eupthres  16864  eupth2lem3lem6fi  16878  subctctexmid  17196  wexmiddifxy  17212  nnnninfex  17231