Theorem 3bitr4g 303

Description: More general version of 3bitr4i 292. 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 272	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	syl6bbr 278	1 |- ( ph -> ( th <-> ta ) )

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

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

This theorem is referenced by:  bibi1d  333  pm5.32rd  672  orbi2d  738  orbi1d  739  ifpbi123d  1027  3orbi123d  1398  3anbi123d  1399  nanbi1  1455  nanbi2  1456  xorbi12d  1478  hadbi123d  1534  had0  1543  cadbi123d  1549  nfbiit  1777  19.23t  2079  nfbidf  2092  nfbidfOLD  2201  19.23tOLD  2218  cbvexd  2278  drex1  2327  drnf1  2329  drsb1  2377  eujustALT  2473  eubid  2488  mobid  2489  eqeq1d  2624  eqeq1dALT  2625  eqeq2d  2632  eleq1w  2684  eleq2w  2685  eleq1d  2686  eleq2d  2687  eleq2dALT  2688  nfceqdf  2760  drnfc1  2782  drnfc2  2783  neleq12d  2901  r19.21t  2955  ralbida  2982  ralbidv2  2984  r19.23t  3021  rexbida  3047  rexbidv2  3048  ralcom2  3104  reubida  3124  rmobida  3129  raleqf  3134  rexeqf  3135  reueq1f  3136  rmoeq1f  3137  cbvraldva2  3175  cbvrexdva2  3176  dfsbcq  3437  sbceqbid  3442  sbcbi2  3484  sbcbid  3489  eqsbc3r  3492  sbcrext  3511  sbcrextOLD  3512  sbcabel  3517  psseq1  3694  psseq2  3695  ssconb  3743  uneq1  3760  ineq1  3807  difin2  3890  reuun2  3910  sbcnel12g  3985  sbnfc2  4007  reldisj  4020  undif4  4035  disjssun  4036  pssdifcom1  4054  pssdifcom2  4055  sbcssg  4085  eltpg  4227  raltpg  4236  rextpg  4237  r19.12sn  4255  intmin4  4506  dfiun2g  4552  iindif2  4589  iinin2  4590  disjprg  4648  disjxun  4651  breq  4655  breq1  4656  breq2  4657  treq  4758  reusv2lem5  4873  rexxfrd  4881  rexxfr2d  4883  rexxfrd2  4885  rabxfrd  4889  opthg2  4948  oteqex2  4963  oteqex  4964  poeq1  5038  soeq1  5054  freq1  5084  weeq1  5102  weeq2  5103  opthprc  5167  wesn  5190  releq  5201  sbcrel  5205  eqrel  5209  eqrelrel  5221  xpiindi  5257  brcnvg  5303  dfres3  5403  brresg  5405  resieq  5407  dmsnopg  5606  dfco2a  5635  ordeq  5730  limeq  5735  ordunisssuc  5830  iotaeq  5859  sniota  5878  sbcfung  5912  imadif  5973  fneq1  5979  fneq2  5980  feq1  6026  feq2  6027  feq3  6028  sbcfng  6042  sbcfg  6043  f1eq1  6096  f1eq2  6097  f1eq3  6098  foeq1  6111  foeq2  6112  foeq3  6113  f1oeq1  6127  f1oeq2  6128  f1oeq3  6129  mpteqb  6299  rexrnmpt  6369  dffo3  6374  fmptco  6396  dff13  6512  f1imaeq  6522  f1imapss  6523  cbvexfo  6545  f1eqcocnv  6556  fliftcnv  6561  isoeq1  6567  isoeq2  6568  isoeq3  6569  isoeq4  6570  isoeq5  6571  isomin  6587  isowe  6599  fnotovb  6694  mpt2eq123  6714  rexrnmpt2  6776  iunpw  6978  tfinds  7059  fun11iun  7126  opiota  7229  ottpos  7362  dmtpos  7364  onoviun  7440  smoeq  7447  smoiso2  7466  tfr2b  7492  oarec  7642  oeeui  7682  nnacan  7708  nnmcan  7714  ereq1  7749  ereq2  7750  elecg  7785  ereldm  7790  ixpiin  7934  boxriin  7950  boxcutc  7951  omxpenlem  8061  nnsdomo  8155  enfi  8176  isfinite2  8218  ixpfi2  8264  elfi2  8320  fipwss  8335  ennum  8773  cardsdom2  8814  aleph11  8907  alephiso  8921  fin23lem26  9147  compssiso  9196  isf34lem4  9199  isfin5-2  9213  fin1a2lem5  9226  brdom7disj  9353  brdom6disj  9354  fpwwe2lem8  9459  fpwwe2lem12  9463  fpwwe2lem13  9464  genpass  9831  ltasr  9921  axpre-lttri  9986  infm3  10982  creur  11014  eqreznegel  11774  rpneg  11863  ltxr  11949  icoshftf1o  12295  elfzm11  12411  elfzomelpfzo  12572  nn0ennn  12778  nnesq  12988  hashbclem  13236  hashf1lem1  13239  leiso  13243  fz1isolem  13245  pr2pwpr  13261  repsdf2  13525  dfrtrclrec2  13797  rexfiuz  14087  cau4  14096  ello1mpt2  14253  o1lo1  14268  fsumcom2  14505  fsumcom2OLD  14506  incexc2  14570  fprodcom2  14714  fprodcom2OLD  14715  dvdsflip  15039  bitsmod  15158  bitscmp  15160  smueqlem  15212  ncoprmgcdne1b  15363  divgcdcoprm0  15379  hashdvds  15480  prmreclem2  15621  vdwapun  15678  vdwmc2  15683  imasaddfnlem  16188  comfeq  16366  oppcsect  16438  funcres2b  16557  funcpropd  16560  fullpropd  16580  fthpropd  16581  fthres2b  16590  fthres2c  16591  fullres2c  16599  ffthres2c  16600  fucsect  16632  fucinv  16633  setcsect  16739  tosso  17036  pospropd  17134  odulatb  17143  oduclatb  17144  isipodrs  17161  odudlatb  17196  issgrpv  17286  issgrpn0  17287  mndpropd  17316  mhmpropd  17341  issubm2  17348  grppropd  17437  grpinvcnv  17483  conjghm  17691  conjnmzb  17695  ghmpropd  17698  gapm  17739  symg1bas  17816  pmtrfrn  17878  cmnpropd  18202  ablpropd  18203  eqgabl  18240  gsumcom2  18374  dmdprd  18397  dprdw  18409  subgdmdprd  18433  pgpfac1lem2  18474  pgpfac1lem4  18477  ringpropd  18582  crngpropd  18583  crngunit  18662  unitpropd  18697  isnirred  18700  drngpropd  18774  fldpropd  18775  subrgpropd  18814  rhmpropd  18815  abvpropd  18842  lmodprop2d  18925  lsspropd  19017  lmhmpropd  19073  lbspropd  19099  lvecprop2d  19166  lvecpropd  19167  opprdomn  19301  fiidomfld  19308  assapropd  19327  psrbagconf1o  19374  mplmonmul  19464  phlpropd  20000  mat1dimbas  20278  tpspropd  20742  tgss2  20791  lmbr2  21063  ist1-2  21151  ist1-3  21153  subislly  21284  dissnlocfin  21332  iskgen3  21352  txcnmpt  21427  hausdiag  21448  hauseqlcld  21449  xkococnlem  21462  tgqtop  21515  txhmeo  21606  uffix2  21728  ufildr  21735  txflf  21810  tgphaus  21920  qustgplem  21924  qustgphaus  21926  xpsdsval  22186  blin  22226  blres  22236  xmeterval  22237  xmspropd  22278  mspropd  22279  setsms  22285  metequiv  22314  metustsym  22360  restmetu  22375  ngppropd  22441  xrtgioo  22609  metdsge  22652  icopnfcnv  22741  iccpnfcnv  22743  lmhmclm  22887  lmmbr  23056  equivcmet  23114  cmspropd  23146  iunmbl2  23325  ioombl1lem4  23329  mbfaddlem  23427  i1fmullem  23461  itg1mulc  23471  iblcnlem1  23554  iblrelem  23557  iblre  23560  iblcn  23565  limcun  23659  mvth  23755  ofmulrt  24037  resinf1o  24282  quad2  24566  1cubr  24569  dcubic  24573  wilthlem2  24795  dvdsflf1o  24913  dvdsflsumcom  24914  fsumvma  24938  vmasum  24941  logfac2  24942  logfaclbnd  24947  dchrelbas3  24963  lgsquadlem1  25105  lgsquadlem2  25106  ax5seg  25818  ushgredgedg  26121  ushgredgedgloop  26123  nbumgrvtx  26242  upgriswlk  26537  rusgrnumwwlkb0  26866  isclwwlksnx  26889  clwwlksnscsh  26940  0trl  26983  0spth  26987  0clwlk  26991  0crct  26993  0cycl  26994  eupth2lem2  27079  eucrct2eupth  27105  fusgr2wsp2nb  27198  numclwwlkovfel2  27216  ocin  28155  chpsscon3  28362  chscllem2  28497  adjval  28749  pjimai  29035  mdsldmd1i  29190  elat2  29199  mdsymi  29270  sbceqbidf  29321  rmoxfrdOLD  29332  rmoxfrd  29333  disjrdx  29404  eqrelrd2  29426  fmptcof2  29457  ofpreima  29465  funcnv5mpt  29469  1stpreima  29484  2ndpreima  29485  fpwrelmapffslem  29507  smatrcl  29862  locfinreflem  29907  zhmnrg  30011  qqhval2  30026  ismntop  30070  reprsuc  30693  reprdifc  30705  bnj919  30837  bnj956  30847  bnj976  30848  bnj1366  30900  bnj916  31003  dfpo2  31645  eqfunresadj  31659  sscoid  32020  dfrdg4  32058  altopthbg  32075  broutsideof3  32233  bj-ssbequ  32629  bj-cbvexdv  32736  bj-drex1v  32749  bj-drnf1v  32750  bj-ax8  32887  bj-restuni  33050  wl-nanbi1  33300  wl-nanbi2  33301  wl-sb8eut  33359  wl-sb8mot  33360  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem25  33434  ftc1anclem5  33489  istotbnd3  33570  sstotbnd  33574  heibor  33620  isass  33645  isidlc  33814  smprngopr  33851  brvvdif  34027  elecALTV  34030  brresALTV  34032  eqrel2  34068  dmecd  34074  relcnveq2  34094  islshpsm  34267  lcvexchlem1  34321  opcon1b  34485  isat3  34594  glbconN  34663  cdleme32fva  35725  cdlemg2cex  35879  dibelval3  36436  dib1dim  36454  doch11  36662  dochsordN  36663  mapdordlem1a  36923  mapd11  36928  mapdsord  36944  mapdcnv11N  36948  mapd0  36954  mrefg2  37270  jm2.23  37563  wepwsolem  37612  dnwech  37618  islssfg2  37641  gicabl  37669  acsfn1p  37769  isdomn3  37782  ifpbi2  37811  ifpbi3  37812  ifpbi23  37817  ifpbi1  37822  ifpbi12  37833  ifpbi13  37834  ifpbi123  37835  pwinfig  37866  inintabd  37885  cnvcnvintabd  37906  cnvintabd  37909  intimag  37948  briunov2  37974  heeq12  38070  sbcheg  38073  rcompleq  38318  uneqsn  38321  ntrneineine0lem  38381  ntrneineine1lem  38382  ntrneik2  38390  ntrneix2  38391  ntrneik13  38396  ntrneix13  38397  ralbidar  38649  rexbidar  38650  trsbc  38750  dffo3f  39364  iccintsng  39749  xlimres  40047  dfateq12d  41209  aov0nbovbi  41275  fnotaovb  41278  sprsymrelf  41745  mgmhmpropd  41785  rngcsect  41980  rngcsectALTV  41992  ringcsect  42031  ringcsectALTV  42055  lindslinindsimp2lem5  42251