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  1288  3anbi123d  1289  nanbi1  1341  nanbi2  1342  xorbi12d  1364  hadbi123d  1423  cadbi123d  1424  cad1  1440  had0  1445  nfbidf  1821  cbvexd  1974  drex1  2019  drnf1  2021  drsb1  2068  sbal2OLD  2184  eujustALT  2256  eubid  2274  mobid  2275  eqeq1  2449  eqeq2  2452  eleq1  2503  eleq2  2504  nfceqdf  2584  drnfc1  2607  drnfc2  2608  neeq1OLD  2645  neeq2OLD  2647  neleq1  2730  neleq2  2731  ralbida  2750  rexbida  2751  ralbidv2  2758  rexbidv2  2759  r19.21t  2822  r19.23t  2852  ralcom2  2906  reubida  2924  rmobida  2929  raleqf  2934  rexeqf  2935  reueq1f  2936  rmoeq1f  2937  cbvraldva2  2972  cbvrexdva2  2973  dfsbcq  3209  sbceqbid  3214  sbcbid  3265  sbcrextOLD  3289  sbcrext  3290  sbcabel  3296  psseq1  3464  psseq2  3465  ssconb  3510  uneq1  3524  ineq1  3566  difin2  3633  reuun2  3654  sbcnel12g  3699  sbnfc2  3727  reldisj  3743  undif4  3756  disjssun  3757  pssdifcom1  3785  pssdifcom2  3786  sbcssg  3811  eltpg  3939  raltpg  3948  rextpg  3949  intmin4  4178  dfiun2g  4223  iindif2  4260  iinin2  4261  disjprg  4309  disjxun  4311  breq  4315  breq1  4316  breq2  4317  treq  4412  reusv2lem5  4518  reusv5OLD  4523  reusv7OLD  4525  rexxfrd  4528  rexxfr2d  4530  rabxfrd  4534  opthg2  4590  oteqex2  4604  oteqex  4605  poeq1  4665  soeq1  4681  freq1  4711  weeq1  4729  weeq2  4730  ordeq  4747  limeq  4752  ordunisssuc  4842  opthprc  4907  wesn  4931  releq  4943  sbcrel  4947  eqrel  4950  eqrelrel  4962  xpiindi  4996  brcnvg  5041  brresg  5140  resieq  5142  dmsnopg  5331  dfco2a  5359  iotaeq  5410  sniota  5429  sbcfung  5462  imadif  5514  fneq1  5520  fneq2  5521  feq1  5563  feq2  5564  feq3  5565  sbcfng  5577  sbcfg  5578  f1eq1  5622  f1eq2  5623  f1eq3  5624  foeq1  5637  foeq2  5638  foeq3  5639  f1oeq1  5653  f1oeq2  5654  f1oeq3  5655  mpteqb  5809  rexrnmpt  5874  dffo3  5879  fmptco  5897  dff13  5992  f1imaeq  5999  f1imapss  6000  cbvexfo  6015  f1eqcocnv  6020  fliftcnv  6025  isoeq1  6031  isoeq2  6032  isoeq3  6033  isoeq4  6034  isoeq5  6035  isomin  6049  isowe  6061  fnotovb  6150  mpt2eq123  6166  rexrnmpt2  6227  iunpw  6411  tfinds  6491  fun11iun  6558  opiota  6654  ottpos  6776  dmtpos  6778  onoviun  6825  smoeq  6832  smoiso2  6851  tfr2b  6876  oarec  7022  oeeui  7062  nnacan  7088  nnmcan  7094  ereq1  7129  ereq2  7130  elecg  7160  ereldm  7165  ixpiin  7310  boxriin  7326  boxcutc  7327  omxpenlem  7433  nnsdomo  7526  enfi  7550  isfinite2  7591  ixpfi2  7630  elfi2  7685  fipwss  7700  ennum  8138  cardsdom2  8179  aleph11  8275  alephiso  8289  fin23lem26  8515  compssiso  8564  isf34lem4  8567  isfin5-2  8581  fin1a2lem5  8594  brdom7disj  8719  brdom6disj  8720  fpwwe2lem8  8825  fpwwe2lem12  8829  fpwwe2lem13  8830  genpass  9199  ltasr  9288  axpre-lttri  9353  infm3  10310  creur  10337  eqreznegel  10961  rpneg  11041  ltxr  11116  icoshftf1o  11429  elfzm11  11549  elfzomelpfzo  11650  nn0ennn  11822  nnesq  12009  pr2pwpr  12204  hashbclem  12226  hashf1lem1  12229  leiso  12233  fz1isolem  12235  repsdf2  12437  rexfiuz  12856  cau4  12865  ello1mpt2  13021  o1lo1  13036  fsumcom2  13262  incexc2  13322  bitsmod  13653  bitscmp  13655  smueqlem  13707  hashdvds  13871  prmreclem2  13999  vdwapun  14056  vdwmc2  14061  imasaddfnlem  14487  comfeq  14666  oppcsect  14733  funcres2b  14828  funcpropd  14831  fullpropd  14851  fthpropd  14852  fthres2b  14861  fthres2c  14862  fullres2c  14870  ffthres2c  14871  fucsect  14903  fucinv  14904  setcsect  14978  tosso  15227  pospropd  15325  odulatb  15334  oduclatb  15335  isipodrs  15352  odudlatb  15387  mndpropd  15467  mhmpropd  15491  issubm2  15497  grppropd  15577  grpinvcnv  15615  conjghm  15798  conjnmzb  15802  ghmpropd  15805  gapm  15845  symg1bas  15922  pmtrfrn  15985  cmnpropd  16307  ablpropd  16308  eqgabl  16340  gsumcom2  16489  dmdprd  16502  dprdw  16516  dprdwOLD  16522  subgdmdprd  16553  pgpfac1lem2  16598  pgpfac1lem4  16601  rngpropd  16698  crngpropd  16699  crngunit  16776  unitpropd  16811  isnirred  16814  drngpropd  16881  fldpropd  16882  subrgpropd  16921  rhmpropd  16922  abvpropd  16949  lmodprop2d  17029  lsspropd  17120  lmhmpropd  17176  lbspropd  17202  lvecprop2d  17269  lvecpropd  17270  rrgsuppOLD  17385  opprdomn  17395  fiidomfld  17402  assapropd  17420  psrbagconf1o  17466  mplmonmul  17565  phlpropd  18106  eltopspOLD  18545  istps2OLD  18548  tpspropd  18567  tgss2  18614  lmbr2  18885  ist1-2  18973  ist1-3  18975  subislly  19107  iskgen3  19144  txcnmpt  19219  hausdiag  19240  hauseqlcld  19241  xkococnlem  19254  tgqtop  19307  txhmeo  19398  uffix2  19519  ufildr  19526  txflf  19601  tgphaus  19709  divstgplem  19713  divstgphaus  19715  xpsdsval  19978  blin  20018  blres  20028  xmeterval  20029  xmspropd  20070  mspropd  20071  setsms  20077  metequiv  20106  metustsymOLD  20158  metustsym  20159  restmetu  20184  ngppropd  20245  xrtgioo  20405  metdsge  20447  icopnfcnv  20536  iccpnfcnv  20538  lmhmclm  20680  lmmbr  20791  equivcmet  20848  cmspropd  20882  iunmbl2  21060  ioombl1lem4  21064  mbfaddlem  21160  i1fmullem  21194  itg1mulc  21204  iblcnlem1  21287  iblrelem  21290  iblre  21293  iblcn  21298  limcun  21392  mvth  21486  ofmulrt  21770  resinf1o  22014  quad2  22256  1cubr  22259  dcubic  22263  wilthlem2  22429  dvdsflip  22544  dvdsflf1o  22549  dvdsflsumcom  22550  fsumvma  22574  vmasum  22577  logfac2  22578  logfaclbnd  22583  dchrelbas3  22599  lgsquadlem1  22715  lgsquadlem2  22716  ax5seg  23206  eupath2lem2  23621  isass  23825  ocin  24721  chpsscon3  24928  chscllem2  25063  adjval  25316  pjimai  25602  mdsldmd1i  25757  elat2  25766  mdsymi  25837  sbceqbidf  25887  rmoxfrdOLD  25898  rmoxfrd  25899  disjrdx  25955  eqrelrd2  25968  fmptcof2  26001  funcnv5mpt  26010  1stpreima  26023  2ndpreima  26024  fpwrelmapffslem  26054  zhmnrg  26418  qqhval2  26433  dfrtrclrec2  27367  fprodcom2  27517  dfpo2  27587  dfres3  27591  sscoid  27966  dfrdg4  28003  altopthbg  28021  broutsideof3  28179  wl-sb8eut  28424  wl-sb8mot  28425  ftc1anclem5  28497  istotbnd3  28696  sstotbnd  28700  heibor  28746  isidlc  28841  smprngopr  28878  mrefg2  29069  jm2.23  29371  wepwsolem  29420  dnwech  29427  islssfg2  29450  gicabl  29480  acsfn1p  29582  isdomn3  29598  ralbidar  29727  rexbidar  29728  dfateq12d  30061  aov0nbovbi  30127  fnotaovb  30130  rexxfrd2  30164  el2wlkonotot1  30419  2pthwlkonot  30430  Lemma2  30519  rusgranumwlkb0  30597  usg2spot2nb  30684  numclwwlkovfel2  30702  mat1dimbas  30907  lindslinindsimp2lem5  30993  trsbc  31343  bnj919  31856  bnj956  31866  bnj976  31867  bnj1366  31919  bnj916  32022  bj-nfbi  32255  bj-cbvexdv  32333  bj-drex1v  32358  bj-drnf1v  32359  bj-eleq1w  32453  bj-eleq2w  32454  islshpsm  32721  lcvexchlem1  32775  opcon1b  32939  isat3  33048  glbconN  33117  cdleme32fva  34177  cdlemg2cex  34331  dibelval3  34888  dib1dim  34906  doch11  35114  dochsordN  35115  mapdordlem1a  35375  mapd11  35380  mapdsord  35396  mapdcnv11N  35400  mapd0  35406