Theorem anbi1d 741

Description: Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
bid.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
anbi1d	|- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )

Proof of Theorem anbi1d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	a1d 25	. 2 |- ( ph -> ( th -> ( ps <-> ch ) ) )
3	2	pm5.32rd 672	1 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  anbi1  743  anbi12d  747  bi2anan9  917  pm5.71  977  cador  1547  drsb1  2377  eleq1w  2684  eleq1d  2686  rexeqf  3135  reueq1f  3136  rmoeq1f  3137  rabeqf  3190  vtocl2gaf  3273  vtocl4ga  3278  alexeqg  3332  elrabi  3359  reu2eqd  3403  sbc2or  3444  sbc5  3460  rexss  3669  psstr  3711  ineq1  3807  difin2  3890  r19.28z  4063  rabsnifsb  4257  ssunsn2  4359  preq12bg  4386  prel12g  4387  opeq1  4402  eluni  4439  csbuni  4466  disjxun  4651  mpteq12f  4731  axrep1  4772  axrep2  4773  axrep3  4774  zfrepclf  4777  axsep  4780  axsep2  4782  zfauscl  4783  reusv2lem4  4872  rabxfrd  4889  opthg  4946  otthg  4954  copsexg  4956  euotd  4975  elopab  4983  pocl  5042  xpeq1  5128  elxpi  5130  vtoclr  5164  opbrop  5198  opelresg  5404  resopab2  5448  dflim2  5781  fun11  5963  feq2  6027  f1eq2  6097  f1eq3  6098  foeq2  6112  brprcneu  6184  ssimaexg  6264  dmfco  6272  fndmdif  6321  respreima  6344  isoeq5  6571  isoini  6588  isopolem  6595  f1oiso  6601  f1oiso2  6602  riotaeqdv  6612  oprabid  6677  oprabv  6703  mpt2eq123  6714  mpt2eq123dva  6716  eloprabga  6747  resoprab  6756  resoprab2  6757  elrnmpt2res  6774  ov  6780  ov3  6797  ov6g  6798  ovg  6799  caoftrn  6932  uniuni  6971  limuni3  7052  elxp4  7110  elxp5  7111  opabex3d  7145  opabex3  7146  opiota  7229  eloprabi  7232  mptmpt2opabbrd  7248  cnvf1o  7276  frxp  7287  xporderlem  7288  poxp  7289  fnwelem  7292  suppimacnv  7306  rexsupp  7313  mpt2curryd  7395  smoel2  7460  omeu  7665  oeeui  7682  omabs  7727  omopth  7738  qliftel  7830  brecop  7840  eroveu  7842  erov  7844  ecopovtrn  7850  ixpsnf1o  7948  dom2lem  7995  xpsnen  8044  xpassen  8054  pw2f1olem  8064  xpf1o  8122  unxpdom  8167  domunfican  8233  preleq  8514  zfinf  8536  cantnfs  8563  tcvalg  8614  r0weon  8835  fseqenlem1  8847  acni2  8869  aceq1  8940  aceq0  8941  dfac2a  8952  dfac12lem2  8966  cardcf  9074  cfeq0  9078  cfsuc  9079  cff1  9080  cfss  9087  isf32lem5  9179  fin1a2lem6  9227  zfac  9282  brdom7disj  9353  brdom6disj  9354  axrepnd  9416  axunndlem1  9417  axinfnd  9428  axacndlem5  9433  axacnd  9434  zfcndrep  9436  zfcndinf  9440  zfcndac  9441  pwfseqlem4a  9483  pwfseqlem4  9484  gruina  9640  grothomex  9651  ordpipq  9764  elnpi  9810  genpass  9831  ltprord  9852  reclem2pr  9870  reclem3pr  9871  recexpr  9873  addsrmo  9894  mulsrmo  9895  addsrpr  9896  mulsrpr  9897  ltsosr  9915  mulgt0sr  9926  supsr  9933  ltresr  9961  axpre-lttrn  9987  axpre-mulgt0  9989  prime  11458  peano5uzti  11467  rexuz  11738  ltxr  11949  qbtwnre  12030  xmulneg1  12099  supxr2  12144  ixxval  12183  fzval  12328  preduz  12461  nn0opth2  13059  hashbclem  13236  hashf1lem2  13240  eqwrd  13346  swrdeq  13444  wrd2ind  13477  cshwcsh2id  13574  eqwrds3  13704  cleq1lem  13721  rtrclreclem3  13800  rtrclreclem4  13801  relexpindlem  13803  abslt  14054  absle  14055  lenegsq  14060  abs2difabs  14074  ello12  14247  elo12  14258  o1lo1  14268  rlimuni  14281  lo1resb  14295  o1resb  14297  2clim  14303  rlimcn2  14321  climcn2  14323  addcn2  14324  mulcn2  14326  o1of2  14343  sumeq1  14419  fsum2dlem  14501  modfsummod  14526  prodeq1f  14638  fprod2dlem  14710  znnenlem  14940  nndivdvds  14989  divalg2  15128  smupval  15210  gcdval  15218  gcdass  15264  lcmval  15305  lcmass  15327  rpexp  15432  pythagtriplem2  15522  pythagtrip  15539  vdwapun  15678  0ram  15724  ramub1lem2  15731  pwsle  16152  imasleval  16201  ismre  16250  ismri  16291  iscatd2  16342  dfiso2  16432  isssc  16480  funcpropd  16560  fullpropd  16580  fthres2b  16590  fthres2c  16591  setcsect  16739  prslem  16931  drsdir  16935  posi  16950  tosso  17036  ipoval  17154  ipolt  17159  odudlatb  17196  dirge  17237  gsumpropd2lem  17273  issgrpv  17286  issgrpn0  17287  mhmpropd  17341  mrcmndind  17366  mgmnsgrpex  17418  issubg3  17612  isga  17724  symgfixelq  17853  psgnfval  17920  psgnval  17927  isslw  18023  dprdw  18409  subgdmdprd  18433  drngpropd  18774  issubrg  18780  islmod  18867  lmodlema  18868  lmodprop2d  18925  lsslss  18961  lbspropd  19099  lbsacsbs  19156  aspval2  19347  psrbag  19364  pf1ind  19719  znleval  19903  islbs4  20171  islinds3  20173  mdetunilem4  20421  mdetunilem9  20426  istopg  20700  basis2  20755  tg2  20769  iscld  20831  neival  20906  isnei  20907  isneip  20909  neiptoptop  20935  neiptopnei  20936  neitr  20984  restlp  20987  iscn  21039  cnpval  21040  iscnp  21041  regsep  21138  1stcclb  21247  2ndc1stc  21254  2ndcctbss  21258  2ndcdisj  21259  llyi  21277  nllyi  21278  hausmapdom  21303  locfinnei  21326  comppfsc  21335  elkgen  21339  txbas  21370  txcls  21407  txcnpi  21411  ptpjopn  21415  txdis1cn  21438  txtube  21443  txcmplem1  21444  hausdiag  21448  tx1stc  21453  txkgen  21455  xkococnlem  21462  xkococn  21463  elqtop  21500  kqreglem1  21544  elmptrab  21630  isfbas  21633  elflim2  21768  elflim  21775  hauspwpwf1  21791  alexsublem  21848  ghmcnp  21918  qustgplem  21924  tsmssubm  21946  elutop  22037  ustuqtop4  22048  isucn  22082  iscfilu  22092  ispsmet  22109  ismet  22128  isxmet  22129  ismet2  22138  imasdsf1olem  22178  blres  22236  elmopn  22247  mopni  22297  neibl  22306  nrmmetd  22379  ngppropd  22441  elcncf  22692  mulc1cncf  22708  elpi1  22845  isclmp  22897  metcld2  23105  pmltpclem1  23217  ovolval  23242  itg1climres  23481  itg2val  23495  isibl  23532  itgeq1f  23538  itgresr  23545  iblcn  23565  itgfsum  23593  dvreslem  23673  dvfsumlem2  23790  deg1ldg  23852  vieta1  24067  ulm2  24139  sincosq2sgn  24251  sincosq4sgn  24253  efopn  24404  dvdsflsumcom  24914  fsumvma2  24939  logfac2  24942  dchrptlem1  24989  lgsdchrval  25079  2lgslem1a  25116  pntibndlem3  25281  pntlemi  25293  pntleme  25297  pnt3  25301  istrkgld  25358  istrkg2ld  25359  istrkg3ld  25360  axtgsegcon  25363  axtg5seg  25364  axtgpasch  25366  axtgupdim2  25370  legov  25480  islnopp  25631  ishpg  25651  iscgra1  25702  brcgr  25780  brbtwn2  25785  axsegconlem1  25797  axsegcon  25807  axcontlem10  25853  edgssv2  26090  uhgr2edg  26100  isfusgrf1  26212  edgnbusgreu  26269  cplgr3v  26331  vtxdun  26377  upgr2wlk  26564  upgrtrls  26598  upgristrl  26599  upgrf1istrl  26600  2pthnloop  26627  usgr2pth  26660  isclwlke  26673  isclwlkupgr  26674  iswwlksnx  26731  wlknewwlksn  26773  wwlksnfi  26801  wspthsnwspthsnon  26811  2pthon3v  26839  wwlks2onv  26847  elwwlks2on  26852  wpthswwlks2on  26854  rusgrnumwwlkl1  26863  rusgrnumwwlkb0  26866  clwwlksel  26914  clwwlksf  26915  erclwwlksnsym  26947  erclwwlksntr  26948  clwlksfoclwwlk  26963  0trl  26983  0spth  26987  0crct  26993  0cycl  26994  upgr4cycl4dv4e  27045  upgriseupth  27067  eupth2lem2  27079  3cyclfrgrrn1  27149  4cycl2vnunb  27154  frgrncvvdeqlem2  27164  frgr2wwlk1  27193  fusgr2wsp2nb  27198  numclwwlkovfel2  27216  vciOLD  27416  isvclem  27432  nmoofval  27617  isph  27677  norm3lemt  28009  isch2  28080  cmbr  28443  eigre  28694  eigorth  28697  nmopub  28767  nmfnleub  28784  cvbr  29141  mdbr  29153  dmdbr  29158  chrelat2  29229  mdsymlem2  29263  rexunirn  29331  ifeqeqx  29361  funcnvmptOLD  29467  funcnvmpt  29468  1stpreima  29484  fpwrelmapffslem  29507  isomnd  29701  archirng  29742  isslmd  29755  slmdlema  29756  orngmul  29803  dya2iocuni  30345  omsfval  30356  elcarsg  30367  itgeq12dv  30388  isrrvv  30505  reprinrn  30696  reprdifc  30705  istrkg2d  30744  axtgupdim2OLD  30746  brafs  30750  bnj956  30847  bnj1146  30862  bnj18eq1  30997  kur14  31198  pconncn  31206  cnpconn  31212  txpconn  31214  cvmscbv  31240  cvmcov  31245  cvmsi  31247  cvmsval  31248  cvmopnlem  31260  cvmlift2lem10  31294  cvmlift3lem2  31302  cvmlift3lem6  31306  cvmlift3lem7  31307  cvmlift3lem9  31309  cvmlift3  31310  mclsssvlem  31459  mclsind  31467  eldm3  31651  opelco3  31678  fv1stcnv  31680  fv2ndcnv  31681  dfon2lem6  31693  dfon2lem7  31694  dfon2lem8  31695  dfon2  31697  poseq  31750  soseq  31751  sltval  31800  nolt02o  31845  slelttr  31882  nocvxminlem  31893  elfuns  32022  brsuccf  32048  brofs  32112  5segofs  32113  brifs  32150  ifscgr  32151  brcolinear  32166  lineext  32183  brfs  32186  fscgr  32187  linecgr  32188  btwnconn1lem4  32197  btwnconn1lem8  32201  btwnconn1lem11  32204  btwnconn1lem12  32205  segcon2  32212  brsegle  32215  outsideofeq  32237  funray  32247  funline  32249  fvline  32251  linethru  32260  trer  32310  finminlem  32312  ivthALT  32330  filnetlem4  32376  knoppndvlem21  32523  bj-axrep1  32788  bj-axrep2  32789  bj-axrep3  32790  bj-axsep  32793  bj-ax8  32887  bj-rabeqd  32916  bj-axsep2  32921  csboprabg  33176  topdifinffinlem  33195  icoreval  33201  isbasisrelowllem1  33203  isbasisrelowllem2  33204  relowlssretop  33211  wl-ax11-lem8  33369  curf  33387  ptrest  33408  poimirlem1  33410  poimirlem13  33422  poimirlem14  33423  poimirlem22  33431  poimirlem24  33433  poimirlem26  33435  poimirlem27  33436  heicant  33444  mblfinlem3  33448  mblfinlem4  33449  mbfresfi  33456  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  areacirclem5  33504  cover2  33508  cover2g  33509  fdc  33541  fdc1  33542  heibor1  33609  bfp  33623  rngosn3  33723  drngoi  33750  isdrngo1  33755  isriscg  33783  isfldidl2  33868  islshpat  34304  lcvbr  34308  lshpsmreu  34396  ldual1dim  34453  cvrval  34556  cvrnbtwn3  34563  iscvlat2N  34611  ishlat3N  34641  hlrelat5N  34687  3dim0  34743  llnexatN  34807  islpln5  34821  islvol5  34865  pmapjat1  35139  ltrnu  35407  cdleme02N  35509  cdlemg33b  35995  cdlemg33c  35996  dvhb1dimN  36274  dibelval3  36436  dibopelval3  36437  dib1dim  36454  dibglbN  36455  diblsmopel  36460  dicval  36465  dicopelval  36466  dicelval3  36469  dicelval1sta  36476  dihopelvalcpre  36537  dih1dimatlem  36618  dihpN  36625  dihjatcclem4  36710  lpolsetN  36771  mapdpglem3  36964  hdmapglem7a  37219  mrefg2  37270  mzpclval  37288  eldiophb  37320  eldioph2lem1  37323  eldioph3  37329  lzenom  37333  diophin  37336  eldiophss  37338  diophrex  37339  eq0rabdioph  37340  pellexlem3  37395  elpell1qr  37411  elpell14qr  37413  elpell1234qr  37415  jm2.27  37575  rmydioph  37581  expdiophlem1  37588  expdioph  37590  pw2f1ocnv  37604  hbtlem1  37693  hbtlem7  37695  dgraalem  37715  dgraaub  37718  ifpbi2  37811  inintabd  37885  cnvcnvintabd  37906  cnvintabd  37909  clcnvlem  37930  iunrelexpmin1  38000  uneqsn  38321  k0004lem2  38446  binomcxplemnotnn0  38555  2sbc6g  38616  2sbc5g  38617  iotasbc  38620  dropab1  38651  dropab2  38652  cbvmpt21  39278  disjinfi  39380  mapsnend  39391  dmrelrnrel  39419  mullimc  39848  mullimcf  39855  limsuppnfd  39934  limsuppnf  39943  limsupre2  39957  limsupre2mpt  39962  limsupre3  39965  limsupre3mpt  39966  limsupre3uzlem  39967  fourierdlem42  40366  fourierdlem48  40371  fourierdlem50  40373  fourierdlem51  40374  fourierdlem54  40377  fourierdlem86  40409  ovnval2  40759  ovnsubaddlem1  40784  hoiqssbl  40839  vonicclem2  40898  dfdfat2  41211  2ffzoeq  41338  pfxeq  41404  mgmhmpropd  41785  ismhm0  41805  isrnghm  41892  rngcsect  41980  rngcinv  41981  rngcsectALTV  41992  rngcinvALTV  41993  ringcsect  42031  ringcinv  42032  ringcsectALTV  42055  ringcinvALTV  42056  lmod1  42281  elbigo2  42346