Theorem 3bitr4g 296

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

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

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 190

This theorem is referenced by:  bibi1d  325  pm5.32rd  650  orbi2d  713  orbi1d  714  3orbi123d  1347  3anbi123d  1348  nanbi1  1406  nanbi2  1407  xorbi12d  1432  ifpbi123d  1450  hadbi123d  1508  had0  1517  cadbi123d  1523  nfbidf  1975  19.23t  2001  cbvexd  2129  drex1  2171  drnf1  2173  drsb1  2216  eujustALT  2312  eubid  2327  mobid  2328  eqeq1d  2463  eqeq1dALT  2464  eqeq2d  2471  eleq1d  2523  eleq2d  2524  eleq2dOLD  2525  eleq2dALT  2526  nfceqdf  2598  drnfc1  2619  drnfc2  2620  neleq12d  2739  r19.21t  2796  r19.21tOLD  2797  ralbida  2832  ralbidv2  2834  r19.23t  2876  rexbida  2907  rexbidv2  2908  ralcom2  2966  reubida  2984  rmobida  2989  raleqf  2994  rexeqf  2995  reueq1f  2996  rmoeq1f  2997  cbvraldva2  3034  cbvrexdva2  3035  dfsbcq  3280  sbceqbid  3285  sbcbi2  3327  sbcbid  3332  sbcrext  3352  sbcabel  3356  psseq1  3531  psseq2  3532  ssconb  3577  uneq1  3592  ineq1  3638  difin2  3716  reuun2  3737  sbcnel12g  3785  sbnfc2  3807  reldisj  3819  undif4  3832  disjssun  3833  pssdifcom1  3864  pssdifcom2  3865  sbcssg  3891  eltpg  4025  raltpg  4034  rextpg  4035  r19.12sn  4049  intmin4  4277  dfiun2g  4323  iindif2  4360  iinin2  4361  disjprg  4411  disjxun  4413  breq  4417  breq1  4418  breq2  4419  treq  4516  reusv2lem5  4621  rexxfrd  4628  rexxfr2d  4630  rabxfrd  4634  opthg2  4692  oteqex2  4706  oteqex  4707  poeq1  4776  soeq1  4792  freq1  4822  weeq1  4840  weeq2  4841  opthprc  4900  wesn  4924  releq  4935  sbcrel  4939  eqrel  4942  eqrelrel  4954  xpiindi  4988  brcnvg  5033  brresg  5131  resieq  5133  dmsnopg  5325  dfco2a  5353  ordeq  5448  limeq  5453  ordunisssuc  5543  iotaeq  5572  sniota  5591  sbcfung  5623  imadif  5679  fneq1  5685  fneq2  5686  feq1  5731  feq2  5732  feq3  5733  sbcfng  5747  sbcfg  5748  f1eq1  5796  f1eq2  5797  f1eq3  5798  foeq1  5811  foeq2  5812  foeq3  5813  f1oeq1  5827  f1oeq2  5828  f1oeq3  5829  mpteqb  5986  rexrnmpt  6054  dffo3  6059  fmptco  6079  dff13  6183  f1imaeq  6190  f1imapss  6191  cbvexfo  6212  f1eqcocnv  6223  fliftcnv  6228  isoeq1  6234  isoeq2  6235  isoeq3  6236  isoeq4  6237  isoeq5  6238  isomin  6252  isowe  6264  fnotovb  6355  mpt2eq123  6376  rexrnmpt2  6438  iunpw  6631  tfinds  6712  fun11iun  6779  opiota  6878  ottpos  7008  dmtpos  7010  onoviun  7087  smoeq  7094  smoiso2  7113  tfr2b  7139  oarec  7288  oeeui  7328  nnacan  7354  nnmcan  7360  ereq1  7395  ereq2  7396  elecg  7427  ereldm  7432  ixpiin  7573  boxriin  7589  boxcutc  7590  omxpenlem  7698  nnsdomo  7792  enfi  7813  isfinite2  7854  ixpfi2  7897  elfi2  7953  fipwss  7968  ennum  8406  cardsdom2  8447  aleph11  8540  alephiso  8554  fin23lem26  8780  compssiso  8829  isf34lem4  8832  isfin5-2  8846  fin1a2lem5  8859  brdom7disj  8984  brdom6disj  8985  fpwwe2lem8  9087  fpwwe2lem12  9091  fpwwe2lem13  9092  genpass  9459  ltasr  9549  axpre-lttri  9614  infm3  10595  creur  10630  eqreznegel  11277  rpneg  11360  ltxr  11443  icoshftf1o  11783  elfzm11  11893  elfzomelpfzo  12043  nn0ennn  12223  nnesq  12427  hashbclem  12647  hashf1lem1  12650  leiso  12654  fz1isolem  12656  pr2pwpr  12668  repsdf2  12917  dfrtrclrec2  13168  rexfiuz  13458  cau4  13467  ello1mpt2  13634  o1lo1  13649  fsumcom2  13883  incexc2  13944  fprodcom2  14086  bitsmod  14458  bitscmp  14460  smueqlem  14512  ncoprmgcdne1b  14703  hashdvds  14771  prmreclem2  14909  vdwapun  14972  vdwmc2  14977  imasaddfnlem  15482  comfeq  15659  oppcsect  15731  funcres2b  15850  funcpropd  15853  fullpropd  15873  fthpropd  15874  fthres2b  15883  fthres2c  15884  fullres2c  15892  ffthres2c  15893  fucsect  15925  fucinv  15926  setcsect  16032  tosso  16330  pospropd  16428  odulatb  16437  oduclatb  16438  isipodrs  16455  odudlatb  16490  issgrpv  16577  issgrpn0  16578  mndpropd  16610  mhmpropd  16636  issubm2  16643  grppropd  16732  grpinvcnv  16770  conjghm  16961  conjnmzb  16965  ghmpropd  16968  gapm  17008  symg1bas  17085  pmtrfrn  17147  cmnpropd  17487  ablpropd  17488  eqgabl  17523  gsumcom2  17655  dmdprd  17678  dprdw  17690  subgdmdprd  17715  pgpfac1lem2  17756  pgpfac1lem4  17759  ringpropd  17860  crngpropd  17861  crngunit  17938  unitpropd  17973  isnirred  17976  drngpropd  18050  fldpropd  18051  subrgpropd  18090  rhmpropd  18091  abvpropd  18118  lmodprop2d  18198  lsspropd  18288  lmhmpropd  18344  lbspropd  18370  lvecprop2d  18437  lvecpropd  18438  opprdomn  18573  fiidomfld  18580  assapropd  18599  psrbagconf1o  18646  mplmonmul  18736  phlpropd  19270  mat1dimbas  19545  tpspropd  20003  tgss2  20051  lmbr2  20323  ist1-2  20411  ist1-3  20413  subislly  20544  dissnlocfin  20592  iskgen3  20612  txcnmpt  20687  hausdiag  20708  hauseqlcld  20709  xkococnlem  20722  tgqtop  20775  txhmeo  20866  uffix2  20987  ufildr  20994  txflf  21069  tgphaus  21179  qustgplem  21183  qustgphaus  21185  xpsdsval  21444  blin  21484  blres  21494  xmeterval  21495  xmspropd  21536  mspropd  21537  setsms  21543  metequiv  21572  metustsym  21618  restmetu  21633  ngppropd  21693  xrtgioo  21872  metdsge  21914  metdsgeOLD  21929  icopnfcnv  22018  iccpnfcnv  22020  lmhmclm  22165  lmmbr  22276  equivcmet  22333  cmspropd  22365  iunmbl2  22558  ioombl1lem4  22562  mbfaddlem  22664  i1fmullem  22700  itg1mulc  22710  iblcnlem1  22793  iblrelem  22796  iblre  22799  iblcn  22804  limcun  22898  mvth  22992  ofmulrt  23283  resinf1o  23533  quad2  23813  1cubr  23816  dcubic  23820  wilthlem2  24042  dvdsflip  24159  dvdsflf1o  24164  dvdsflsumcom  24165  fsumvma  24189  vmasum  24192  logfac2  24193  logfaclbnd  24198  dchrelbas3  24214  lgsquadlem1  24330  lgsquadlem2  24331  ax5seg  25016  clwwlknscsh  25595  el2wlkonotot1  25650  2pthwlkonot  25661  rusgranumwlkb0  25729  eupath2lem2  25754  usg2spot2nb  25841  numclwwlkovfel2  25859  isass  26092  ocin  26997  chpsscon3  27204  chscllem2  27339  adjval  27591  pjimai  27877  mdsldmd1i  28032  elat2  28041  mdsymi  28112  sbceqbidf  28165  rmoxfrdOLD  28176  rmoxfrd  28177  disjrdx  28249  eqrelrd2  28270  fmptcof2  28307  ofpreima  28316  funcnv5mpt  28320  1stpreima  28335  2ndpreima  28336  fpwrelmapffslem  28365  smatrcl  28670  locfinreflem  28715  zhmnrg  28819  qqhval2  28834  ismntop  28878  bnj919  29626  bnj956  29636  bnj976  29637  bnj1366  29689  bnj916  29792  dfpo2  30443  dfres3  30447  sscoid  30728  dfrdg4  30766  altopthbg  30783  broutsideof3  30941  bj-nfbi  31261  bj-ssbequ  31286  bj-cbvexdv  31381  bj-drex1v  31403  bj-drnf1v  31404  bj-eleq1w  31499  bj-eleq2w  31500  bj-ax8  31539  wl-nanbi1  31899  wl-nanbi2  31900  wl-sb8eut  31950  wl-sb8mot  31951  poimirlem17  32001  poimirlem19  32003  poimirlem20  32004  poimirlem25  32009  ftc1anclem5  32065  istotbnd3  32147  sstotbnd  32151  heibor  32197  isidlc  32292  smprngopr  32329  islshpsm  32590  lcvexchlem1  32644  opcon1b  32808  isat3  32917  glbconN  32986  cdleme32fva  34048  cdlemg2cex  34202  dibelval3  34759  dib1dim  34777  doch11  34985  dochsordN  34986  mapdordlem1a  35246  mapd11  35251  mapdsord  35267  mapdcnv11N  35271  mapd0  35277  mrefg2  35593  jm2.23  35895  wepwsolem  35944  dnwech  35950  islssfg2  35973  gicabl  36001  acsfn1p  36109  isdomn3  36125  ifpbi2  36154  ifpbi3  36155  ifpbi23  36160  ifpbi1  36165  ifpbi12  36176  ifpbi13  36177  ifpbi123  36178  pwinfig  36209  inintabd  36229  cnvcnvintabd  36250  cnvintabd  36253  intimag  36292  briunov2  36318  heeq12  36415  sbcheg  36418  ralbidar  36841  rexbidar  36842  trsbc  36944  dffo3f  37487  iccintsng  37661  dfateq12d  38668  aov0nbovbi  38734  fnotaovb  38737  rexxfrd2  39048  ushgredgedga  39355  ushgredgedgaloop  39357  nbumgrvtx  39463  0clWlk  39845  mgmhmpropd  40057  rngcsect  40254  rngcsectALTV  40266  ringcsect  40305  ringcsectALTV  40329  lindslinindsimp2lem5  40527