Theorem 3bitr4g 288

Description: More general version of 3bitr4i 277. Useful for converting definitions in a formula. (Contributed by NM, 11-May-1993.)

Hypotheses

Ref	Expression
3bitr4g.1	|- ( ph -> ( ps <-> ch ) )
3bitr4g.2	|- ( th <-> ps )
3bitr4g.3	|- ( ta <-> ch )

Assertion

Ref	Expression
3bitr4g	|- ( ph -> ( th <-> ta ) )

Proof of Theorem 3bitr4g

Step	Hyp	Ref	Expression
1		3bitr4g.2	. . 3 |- ( th <-> ps )
2		3bitr4g.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3	1, 2	syl5bb 257	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	syl6bbr 263	1 |- ( ph -> ( th <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 184

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 185

This theorem is referenced by:  bibi1d  317  pm5.32rd  638  orbi2d  699  orbi1d  700  3orbi123d  1296  3anbi123d  1297  nanbi1  1353  nanbi2  1354  xorbi12d  1379  hadbi123d  1456  cadbi123d  1457  cad1OLD  1473  had0  1479  nfbidf  1895  cbvexd  2033  drex1  2075  drnf1  2077  drsb1  2122  eujustALT  2221  eubid  2238  mobid  2239  eqeq1d  2384  eqeq1dALT  2385  eqeq1OLD  2387  eqeq2d  2396  eqeq2OLD  2398  eleq1d  2451  eleq2d  2452  eleq2dALT  2453  eleq1OLD  2456  eleq2OLD  2457  nfceqdf  2539  drnfc1  2563  drnfc2  2564  neeq1OLD  2664  neeq2OLD  2666  neleq12d  2719  neleq1OLD  2721  neleq2OLD  2723  r19.21t  2779  r19.21tOLD  2780  ralbida  2815  ralbidv2  2817  r19.23t  2860  rexbida  2888  rexbidv2  2889  ralcom2  2947  reubida  2965  rmobida  2970  raleqf  2975  rexeqf  2976  reueq1f  2977  rmoeq1f  2978  cbvraldva2  3013  cbvrexdva2  3014  dfsbcq  3254  sbceqbid  3259  sbcbi2  3301  sbcbid  3306  sbcrext  3326  sbcabel  3330  psseq1  3505  psseq2  3506  ssconb  3551  uneq1  3565  ineq1  3607  difin2  3685  reuun2  3706  sbcnel12g  3752  sbnfc2  3774  reldisj  3786  undif4  3799  disjssun  3800  pssdifcom1  3829  pssdifcom2  3830  sbcssg  3856  eltpg  3986  raltpg  3995  rextpg  3996  r19.12sn  4009  intmin4  4229  dfiun2g  4275  iindif2  4312  iinin2  4313  disjprg  4363  disjxun  4365  breq  4369  breq1  4370  breq2  4371  treq  4466  reusv2lem5  4570  rexxfrd  4577  rexxfr2d  4579  rabxfrd  4583  opthg2  4639  oteqex2  4653  oteqex  4654  poeq1  4717  soeq1  4733  freq1  4763  weeq1  4781  weeq2  4782  ordeq  4799  limeq  4804  ordunisssuc  4894  opthprc  4961  wesn  4985  releq  4998  sbcrel  5002  eqrel  5005  eqrelrel  5017  xpiindi  5051  brcnvg  5096  brresg  5194  resieq  5196  dmsnopg  5387  dfco2a  5415  iotaeq  5468  sniota  5487  sbcfung  5519  imadif  5571  fneq1  5577  fneq2  5578  feq1  5621  feq2  5622  feq3  5623  sbcfng  5636  sbcfg  5637  f1eq1  5684  f1eq2  5685  f1eq3  5686  foeq1  5699  foeq2  5700  foeq3  5701  f1oeq1  5715  f1oeq2  5716  f1oeq3  5717  mpteqb  5872  rexrnmpt  5943  dffo3  5948  fmptco  5966  dff13  6067  f1imaeq  6074  f1imapss  6075  cbvexfo  6094  f1eqcocnv  6105  fliftcnv  6110  isoeq1  6116  isoeq2  6117  isoeq3  6118  isoeq4  6119  isoeq5  6120  isomin  6134  isowe  6146  fnotovb  6237  mpt2eq123  6255  rexrnmpt2  6317  iunpw  6513  tfinds  6593  fun11iun  6659  opiota  6758  ottpos  6883  dmtpos  6885  onoviun  6932  smoeq  6939  smoiso2  6958  tfr2b  6983  oarec  7129  oeeui  7169  nnacan  7195  nnmcan  7201  ereq1  7236  ereq2  7237  elecg  7268  ereldm  7273  ixpiin  7414  boxriin  7430  boxcutc  7431  omxpenlem  7537  nnsdomo  7631  enfi  7652  isfinite2  7693  ixpfi2  7733  elfi2  7789  fipwss  7804  ennum  8241  cardsdom2  8282  aleph11  8378  alephiso  8392  fin23lem26  8618  compssiso  8667  isf34lem4  8670  isfin5-2  8684  fin1a2lem5  8697  brdom7disj  8822  brdom6disj  8823  fpwwe2lem8  8926  fpwwe2lem12  8930  fpwwe2lem13  8931  genpass  9298  ltasr  9388  axpre-lttri  9453  infm3  10418  creur  10446  eqreznegel  11086  rpneg  11169  ltxr  11245  icoshftf1o  11564  elfzm11  11671  elfzomelpfzo  11813  nn0ennn  11992  nnesq  12192  hashbclem  12405  hashf1lem1  12408  leiso  12412  fz1isolem  12414  pr2pwpr  12424  repsdf2  12661  dfrtrclrec2  12892  rexfiuz  13182  cau4  13191  ello1mpt2  13347  o1lo1  13362  fsumcom2  13591  incexc2  13652  fprodcom2  13790  bitsmod  14088  bitscmp  14090  smueqlem  14142  hashdvds  14307  prmreclem2  14437  vdwapun  14494  vdwmc2  14499  imasaddfnlem  14935  comfeq  15112  oppcsect  15184  funcres2b  15303  funcpropd  15306  fullpropd  15326  fthpropd  15327  fthres2b  15336  fthres2c  15337  fullres2c  15345  ffthres2c  15346  fucsect  15378  fucinv  15379  setcsect  15485  tosso  15783  pospropd  15881  odulatb  15890  oduclatb  15891  isipodrs  15908  odudlatb  15943  issgrpv  16030  issgrpn0  16031  mndpropd  16063  mhmpropd  16089  issubm2  16096  grppropd  16185  grpinvcnv  16223  conjghm  16414  conjnmzb  16418  ghmpropd  16421  gapm  16461  symg1bas  16538  pmtrfrn  16600  cmnpropd  16924  ablpropd  16925  eqgabl  16960  gsumcom2  17117  dmdprd  17142  dprdw  17156  dprdwOLD  17163  subgdmdprd  17194  pgpfac1lem2  17239  pgpfac1lem4  17242  ringpropd  17343  crngpropd  17344  crngunit  17424  unitpropd  17459  isnirred  17462  drngpropd  17536  fldpropd  17537  subrgpropd  17576  rhmpropd  17577  abvpropd  17604  lmodprop2d  17685  lsspropd  17776  lmhmpropd  17832  lbspropd  17858  lvecprop2d  17925  lvecpropd  17926  rrgsuppOLD  18053  opprdomn  18063  fiidomfld  18070  assapropd  18089  psrbagconf1o  18139  mplmonmul  18239  phlpropd  18781  mat1dimbas  19059  eltopspOLD  19504  istps2OLD  19507  tpspropd  19526  tgss2  19574  lmbr2  19846  ist1-2  19934  ist1-3  19936  subislly  20067  dissnlocfin  20115  iskgen3  20135  txcnmpt  20210  hausdiag  20231  hauseqlcld  20232  xkococnlem  20245  tgqtop  20298  txhmeo  20389  uffix2  20510  ufildr  20517  txflf  20592  tgphaus  20700  qustgplem  20704  qustgphaus  20706  xpsdsval  20969  blin  21009  blres  21019  xmeterval  21020  xmspropd  21061  mspropd  21062  setsms  21068  metequiv  21097  metustsymOLD  21149  metustsym  21150  restmetu  21175  ngppropd  21236  xrtgioo  21396  metdsge  21438  icopnfcnv  21527  iccpnfcnv  21529  lmhmclm  21671  lmmbr  21782  equivcmet  21839  cmspropd  21873  iunmbl2  22052  ioombl1lem4  22056  mbfaddlem  22152  i1fmullem  22186  itg1mulc  22196  iblcnlem1  22279  iblrelem  22282  iblre  22285  iblcn  22290  limcun  22384  mvth  22478  ofmulrt  22763  resinf1o  23008  quad2  23286  1cubr  23289  dcubic  23293  wilthlem2  23460  dvdsflip  23575  dvdsflf1o  23580  dvdsflsumcom  23581  fsumvma  23605  vmasum  23608  logfac2  23609  logfaclbnd  23614  dchrelbas3  23630  lgsquadlem1  23746  lgsquadlem2  23747  ax5seg  24362  clwwlknscsh  24940  el2wlkonotot1  24995  2pthwlkonot  25006  rusgranumwlkb0  25074  eupath2lem2  25099  usg2spot2nb  25186  numclwwlkovfel2  25204  isass  25435  ocin  26331  chpsscon3  26538  chscllem2  26673  adjval  26925  pjimai  27211  mdsldmd1i  27366  elat2  27375  mdsymi  27446  sbceqbidf  27497  rmoxfrdOLD  27508  rmoxfrd  27509  disjrdx  27580  eqrelrd2  27601  fmptcof2  27643  ofpreima  27653  funcnv5mpt  27657  1stpreima  27672  2ndpreima  27673  fpwrelmapffslem  27705  locfinreflem  27997  zhmnrg  28101  qqhval2  28116  ismntop  28157  dfpo2  29350  dfres3  29354  sscoid  29716  dfrdg4  29753  altopthbg  29771  broutsideof3  29929  wl-nanbi1  30140  wl-nanbi2  30141  wl-sb8eut  30187  wl-sb8mot  30188  ftc1anclem5  30260  istotbnd3  30433  sstotbnd  30437  heibor  30483  isidlc  30578  smprngopr  30615  mrefg2  30805  jm2.23  31104  wepwsolem  31153  dnwech  31160  islssfg2  31183  gicabl  31215  acsfn1p  31316  isdomn3  31332  ralbidar  31522  rexbidar  31523  iccintsng  31729  dfateq12d  32380  aov0nbovbi  32446  fnotaovb  32449  rexxfrd2  32625  mgmhmpropd  32791  rngcsect  32988  rngcsectALTV  33000  ringcsect  33039  ringcsectALTV  33063  lindslinindsimp2lem5  33263  trsbc  33647  bnj919  34172  bnj956  34182  bnj976  34183  bnj1366  34235  bnj916  34338  bj-nfbi  34564  bj-cbvexdv  34648  bj-drex1v  34674  bj-drnf1v  34675  bj-eleq1w  34769  bj-eleq2w  34770  islshpsm  35118  lcvexchlem1  35172  opcon1b  35336  isat3  35445  glbconN  35514  cdleme32fva  36576  cdlemg2cex  36730  dibelval3  37287  dib1dim  37305  doch11  37513  dochsordN  37514  mapdordlem1a  37774  mapd11  37779  mapdsord  37795  mapdcnv11N  37799  mapd0  37805  ifpbi1  38112  ifpbi2  38113  ifpbi3  38114  ifpbi12  38115  ifpbi13  38116  ifpbi23  38117  ifpbi123  38118  pwinfig  38175  intimag  38200  briunov2  38220  heeq12  38270  sbcheg  38273