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  7329  nninfninc  7463  nnnninfeq2  7469  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  isacnm  7559  acfun  7563  2omotaplemap  7623  2omotaplemst  7624  exmidapne  7626  ccfunen  7630  recexnq  7757  recmulnqg  7758  ltsonq  7765  enq0sym  7799  enq0ref  7800  enq0tr  7801  enq0breq  7803  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  mulnnnq0  7817  elinp  7841  prdisj  7859  prarloclem3  7864  prarloc  7870  distrlem5prl  7953  distrlem5pru  7954  ltexprlemell  7965  ltexprlemelu  7966  recexprlemm  7991  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  lttrsr  8129  recexgt0sr  8140  mulgt0sr  8145  ltresr  8206  axprecex  8247  axpre-lttrn  8251  axpre-mulgt0  8254  eqlelt  8412  lesub0  8808  apreap  8917  apreim  8933  aprcl  8976  aptap  8980  zltlen  9728  prime  9749  fzind  9765  qltlen  10049  xltnegi  10247  ixxval  10308  fzval  10423  fzdifsuc  10498  elfzm11  10508  elfzo  10566  zsupcllemex  10673  exbtwnzlemshrink  10693  rebtwn2zlemshrink  10698  facwordi  11192  zfz1iso  11307  pfxsuff1eqwrdeq  11485  wrd2ind  11509  shftfvalg  11597  shftfibg  11599  shftfval  11600  shftfib  11602  shftfn  11603  2shfti  11610  cau3lem  11895  caubnd2  11898  xrmaxiflemcom  12031  clim  12063  clim2  12065  climi  12069  climcn2  12091  addcn2  12092  subcn2  12093  mulcn2  12094  summodclem2a  12164  summodc  12166  fsum3  12170  fsumsplitf  12191  prodfdivap  12330  ntrivcvgap0  12332  prodeq1f  12335  prodeq2w  12339  prodeq2  12340  prodmodc  12361  zproddc  12362  fprodseq  12366  fprodntrivap  12367  fproddivapf  12414  fprodsplitf  12415  fprodsplit1f  12417  sinbnd  12535  cosbnd  12536  divalgb  12708  ndvdssub  12713  gcdval  12752  gcdneg  12775  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlemex  12794  dfgcd2  12807  gcdass  12808  algcvgblem  12843  lcmval  12857  lcmneg  12868  lcmgcdlem  12871  lcmass  12879  qredeq  12890  prmind2  12914  euclemma  12941  pwbdvdslemn  12960  qnumval  12981  qdenval  12982  pceu  13094  pczpre  13096  pcdiv  13101  prmpwdvds  13154  gzsumress  13761  gzsum0  13762  mnd1  13811  grp1  13960  qusgrp2  13965  nmznsg  14065  releqgg  14072  eqgex  14073  iscmnd  14150  gsumvalfi  14201  prdsex  14221  issrg  14318  iscrng2  14368  qusring2  14420  opprunitd  14466  crngunit  14467  dfrhm2  14510  rhmopp  14532  issubrng  14556  resrhm2b  14606  islmod  14676  lsssetm  14742  lsspropdg  14817  ixpsnbasval  14852  basis2  15198  eltg2  15203  isnei  15294  isneip  15296  restbasg  15318  iscnp  15349  iscnp3  15353  tgcn  15358  icnpimaex  15361  lmbrf  15365  cncnp  15380  cnptoprest2  15390  txbas  15408  txcnp  15421  imasnopn  15449  ispsmet  15473  ismet  15494  isxmet  15495  ismet2  15504  blres  15584  metcnp3  15661  txmetcnp  15668  mulcncf  15758  ellimc3apf  15810  limcdifap  15812  limcmpted  15813  limccnp2lem  15826  dvmptfsum  15875  elply2  15885  sincosq3sgn  15979  zprmlogbaplem3  16136  pellexlem3  16150  lgsquadlem1  16294  2sqlem8  16340  2sqlem9  16341  eupthres  16796  eupth2lem3lem6fi  16810  subctctexmid  17128  wexmiddifxy  17144  nnnninfex  17163