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  319  pm5.32rd  640  orbi2d  701  orbi1d  702  3orbi123d  1298  3anbi123d  1299  nanbi1  1351  nanbi2  1352  xorbi12d  1374  hadbi123d  1433  cadbi123d  1434  cad1  1450  had0  1455  nfbidf  1835  cbvexd  1999  drex1  2042  drnf1  2044  drsb1  2091  sbal2OLD  2206  eujustALT  2278  eubid  2296  mobid  2297  eqeq1d  2469  eqeq1dALT  2470  eqeq1OLD  2472  eqeq2d  2481  eqeq2OLD  2483  eleq1d  2536  eleq2d  2537  eleq2dALT  2538  eleq1OLD  2541  eleq2OLD  2542  nfceqdf  2624  drnfc1  2648  drnfc2  2649  neeq1OLD  2749  neeq2OLD  2751  neleq12d  2804  neleq1OLD  2806  neleq2OLD  2808  r19.21t  2861  r19.21tOLD  2862  ralbida  2897  ralbidv2  2899  r19.23t  2941  rexbida  2968  rexbidv2  2969  ralcom2  3026  reubida  3044  rmobida  3049  raleqf  3054  rexeqf  3055  reueq1f  3056  rmoeq1f  3057  cbvraldva2  3092  cbvrexdva2  3093  dfsbcq  3333  sbceqbid  3338  sbcbid  3389  sbcrextOLD  3413  sbcrext  3414  sbcabel  3420  psseq1  3591  psseq2  3592  ssconb  3637  uneq1  3651  ineq1  3693  difin2  3760  reuun2  3781  sbcnel12g  3826  sbnfc2  3854  reldisj  3870  undif4  3883  disjssun  3884  pssdifcom1  3912  pssdifcom2  3913  sbcssg  3938  eltpg  4069  raltpg  4078  rextpg  4079  intmin4  4311  dfiun2g  4357  iindif2  4394  iinin2  4395  disjprg  4443  disjxun  4445  breq  4449  breq1  4450  breq2  4451  treq  4546  reusv2lem5  4652  reusv5OLD  4657  reusv7OLD  4659  rexxfrd  4662  rexxfr2d  4664  rabxfrd  4668  opthg2  4724  oteqex2  4739  oteqex  4740  poeq1  4803  soeq1  4819  freq1  4849  weeq1  4867  weeq2  4868  ordeq  4885  limeq  4890  ordunisssuc  4980  opthprc  5047  wesn  5071  releq  5085  sbcrel  5089  eqrel  5092  eqrelrel  5104  xpiindi  5138  brcnvg  5183  brresg  5282  resieq  5284  dmsnopg  5479  dfco2a  5507  iotaeq  5559  sniota  5578  sbcfung  5611  imadif  5663  fneq1  5669  fneq2  5670  feq1  5713  feq2  5714  feq3  5715  sbcfng  5728  sbcfg  5729  f1eq1  5776  f1eq2  5777  f1eq3  5778  foeq1  5791  foeq2  5792  foeq3  5793  f1oeq1  5807  f1oeq2  5808  f1oeq3  5809  mpteqb  5964  rexrnmpt  6031  dffo3  6036  fmptco  6054  dff13  6154  f1imaeq  6161  f1imapss  6162  cbvexfo  6181  f1eqcocnv  6192  fliftcnv  6197  isoeq1  6203  isoeq2  6204  isoeq3  6205  isoeq4  6206  isoeq5  6207  isomin  6221  isowe  6233  fnotovb  6323  mpt2eq123  6340  rexrnmpt2  6402  iunpw  6598  tfinds  6678  fun11iun  6744  opiota  6843  ottpos  6965  dmtpos  6967  onoviun  7014  smoeq  7021  smoiso2  7040  tfr2b  7065  oarec  7211  oeeui  7251  nnacan  7277  nnmcan  7283  ereq1  7318  ereq2  7319  elecg  7350  ereldm  7355  ixpiin  7495  boxriin  7511  boxcutc  7512  omxpenlem  7618  nnsdomo  7712  enfi  7736  isfinite2  7778  ixpfi2  7818  elfi2  7874  fipwss  7889  ennum  8328  cardsdom2  8369  aleph11  8465  alephiso  8479  fin23lem26  8705  compssiso  8754  isf34lem4  8757  isfin5-2  8771  fin1a2lem5  8784  brdom7disj  8909  brdom6disj  8910  fpwwe2lem8  9015  fpwwe2lem12  9019  fpwwe2lem13  9020  genpass  9387  ltasr  9477  axpre-lttri  9542  infm3  10502  creur  10530  eqreznegel  11167  rpneg  11249  ltxr  11324  icoshftf1o  11643  elfzm11  11749  elfzomelpfzo  11882  nn0ennn  12057  nnesq  12258  hashbclem  12467  hashf1lem1  12470  leiso  12474  fz1isolem  12476  pr2pwpr  12486  repsdf2  12713  rexfiuz  13143  cau4  13152  ello1mpt2  13308  o1lo1  13323  fsumcom2  13552  incexc2  13613  bitsmod  13945  bitscmp  13947  smueqlem  13999  hashdvds  14164  prmreclem2  14294  vdwapun  14351  vdwmc2  14356  imasaddfnlem  14783  comfeq  14962  oppcsect  15029  funcres2b  15124  funcpropd  15127  fullpropd  15147  fthpropd  15148  fthres2b  15157  fthres2c  15158  fullres2c  15166  ffthres2c  15167  fucsect  15199  fucinv  15200  setcsect  15274  tosso  15523  pospropd  15621  odulatb  15630  oduclatb  15631  isipodrs  15648  odudlatb  15683  mndpropd  15764  mhmpropd  15792  issubm2  15798  grppropd  15878  grpinvcnv  15916  conjghm  16102  conjnmzb  16106  ghmpropd  16109  gapm  16149  symg1bas  16226  pmtrfrn  16289  cmnpropd  16613  ablpropd  16614  eqgabl  16646  gsumcom2  16806  dmdprd  16832  dprdw  16846  dprdwOLD  16852  subgdmdprd  16883  pgpfac1lem2  16928  pgpfac1lem4  16931  rngpropd  17031  crngpropd  17032  crngunit  17112  unitpropd  17147  isnirred  17150  drngpropd  17223  fldpropd  17224  subrgpropd  17263  rhmpropd  17264  abvpropd  17291  lmodprop2d  17372  lsspropd  17463  lmhmpropd  17519  lbspropd  17545  lvecprop2d  17612  lvecpropd  17613  rrgsuppOLD  17739  opprdomn  17749  fiidomfld  17756  assapropd  17775  psrbagconf1o  17825  mplmonmul  17925  phlpropd  18485  mat1dimbas  18769  eltopspOLD  19214  istps2OLD  19217  tpspropd  19236  tgss2  19283  lmbr2  19554  ist1-2  19642  ist1-3  19644  subislly  19776  iskgen3  19813  txcnmpt  19888  hausdiag  19909  hauseqlcld  19910  xkococnlem  19923  tgqtop  19976  txhmeo  20067  uffix2  20188  ufildr  20195  txflf  20270  tgphaus  20378  divstgplem  20382  divstgphaus  20384  xpsdsval  20647  blin  20687  blres  20697  xmeterval  20698  xmspropd  20739  mspropd  20740  setsms  20746  metequiv  20775  metustsymOLD  20827  metustsym  20828  restmetu  20853  ngppropd  20914  xrtgioo  21074  metdsge  21116  icopnfcnv  21205  iccpnfcnv  21207  lmhmclm  21349  lmmbr  21460  equivcmet  21517  cmspropd  21551  iunmbl2  21730  ioombl1lem4  21734  mbfaddlem  21830  i1fmullem  21864  itg1mulc  21874  iblcnlem1  21957  iblrelem  21960  iblre  21963  iblcn  21968  limcun  22062  mvth  22156  ofmulrt  22440  resinf1o  22684  quad2  22926  1cubr  22929  dcubic  22933  wilthlem2  23099  dvdsflip  23214  dvdsflf1o  23219  dvdsflsumcom  23220  fsumvma  23244  vmasum  23247  logfac2  23248  logfaclbnd  23253  dchrelbas3  23269  lgsquadlem1  23385  lgsquadlem2  23386  ax5seg  23945  clwwlknscsh  24523  el2wlkonotot1  24578  2pthwlkonot  24589  rusgranumwlkb0  24657  eupath2lem2  24682  usg2spot2nb  24770  numclwwlkovfel2  24788  isass  25022  ocin  25918  chpsscon3  26125  chscllem2  26260  adjval  26513  pjimai  26799  mdsldmd1i  26954  elat2  26963  mdsymi  27034  sbceqbidf  27084  rmoxfrdOLD  27095  rmoxfrd  27096  disjrdx  27151  eqrelrd2  27168  fmptcof2  27202  funcnv5mpt  27211  1stpreima  27224  2ndpreima  27225  fpwrelmapffslem  27255  zhmnrg  27612  qqhval2  27627  ismntop  27672  dfrtrclrec2  28569  fprodcom2  28719  dfpo2  28789  dfres3  28793  sscoid  29168  dfrdg4  29205  altopthbg  29223  broutsideof3  29381  wl-sb8eut  29627  wl-sb8mot  29628  ftc1anclem5  29699  istotbnd3  29898  sstotbnd  29902  heibor  29948  isidlc  30043  smprngopr  30080  mrefg2  30271  jm2.23  30570  wepwsolem  30619  dnwech  30626  islssfg2  30649  gicabl  30679  acsfn1p  30781  isdomn3  30797  ralbidar  30960  rexbidar  30961  iccintsng  31155  dfateq12d  31709  aov0nbovbi  31775  fnotaovb  31778  rexxfrd2  31799  lindslinindsimp2lem5  32162  trsbc  32409  bnj919  32922  bnj956  32932  bnj976  32933  bnj1366  32985  bnj916  33088  bj-nfbi  33323  bj-cbvexdv  33401  bj-drex1v  33426  bj-drnf1v  33427  bj-eleq1w  33521  bj-eleq2w  33522  islshpsm  33795  lcvexchlem1  33849  opcon1b  34013  isat3  34122  glbconN  34191  cdleme32fva  35251  cdlemg2cex  35405  dibelval3  35962  dib1dim  35980  doch11  36188  dochsordN  36189  mapdordlem1a  36449  mapd11  36454  mapdsord  36470  mapdcnv11N  36474  mapd0  36480