Theorem 3bitr4g 280

Description: More general version of 3bitr4i 269. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-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 249	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	syl6bbr 255	1 |- ( ph -> ( th <-> ta ) )

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

This theorem is referenced by:  bibi1d  311  pm5.32rd  622  orbi2d  683  orbi1d  684  3orbi123d  1253  3anbi123d  1254  nanbi1  1301  nanbi2  1302  xorbi12d  1321  hadbi123d  1388  cadbi123d  1389  cad1  1404  had0  1409  nfbidf  1786  drex1  2024  drnf1  2026  drnf2  2027  cbvexd  2059  drsb1  2071  sbal2  2184  eujustALT  2257  eubid  2261  mobid  2288  eqeq1  2410  eqeq2  2413  eleq1  2464  eleq2  2465  nfceqdf  2539  drnfc1  2556  drnfc2  2557  neeq1  2575  neeq2  2576  neleq1  2660  neleq2  2661  ralbida  2680  rexbida  2681  ralbidv2  2688  rexbidv2  2689  r19.21t  2751  r19.23t  2780  ralcom2  2832  reubida  2850  rmobida  2855  raleqf  2860  rexeqf  2861  reueq1f  2862  rmoeq1f  2863  cbvraldva2  2896  cbvrexdva2  2897  dfsbcq  3123  sbcbid  3174  sbcrext  3194  sbcabel  3198  sbnfc2  3269  psseq1  3394  psseq2  3395  ssconb  3440  uneq1  3454  ineq1  3495  difin2  3563  reuun2  3584  reldisj  3631  undif4  3644  disjssun  3645  pssdifcom1  3673  pssdifcom2  3674  sbcss  3698  eltpg  3811  raltpg  3819  rextpg  3820  intmin4  4039  dfiun2g  4083  iindif2  4120  iinin2  4121  disjprg  4168  disjxun  4170  breq  4174  breq1  4175  breq2  4176  treq  4268  opthg2  4397  oteqex2  4408  oteqex  4409  poeq1  4466  soeq1  4482  freq1  4512  weeq1  4530  weeq2  4531  ordeq  4548  limeq  4553  ordunisssuc  4643  reusv2lem5  4687  reusv5OLD  4692  reusv7OLD  4694  rexxfrd  4697  rexxfr2d  4699  rabxfrd  4703  iunpw  4718  tfinds  4798  opthprc  4884  wesn  4908  releq  4918  eqrel  4924  eqrelrel  4936  xpiindi  4969  brcnvg  5012  brresg  5113  resieq  5115  dmsnopg  5300  dfco2a  5329  iotaeq  5385  sniota  5404  imadif  5487  fneq1  5493  fneq2  5494  feq1  5535  feq2  5536  feq3  5537  f1eq1  5593  f1eq2  5594  f1eq3  5595  foeq1  5608  foeq2  5609  foeq3  5610  f1oeq1  5624  f1oeq2  5625  f1oeq3  5626  fun11iun  5654  mpteqb  5778  rexrnmpt  5838  dffo3  5843  fmptco  5860  dff13  5963  f1imaeq  5970  f1imapss  5971  cbvexfo  5982  f1eqcocnv  5987  fliftcnv  5992  isoeq1  5998  isoeq2  5999  isoeq3  6000  isoeq4  6001  isoeq5  6002  isomin  6016  isowe  6028  fnotovb  6076  mpt2eq123  6092  rexrnmpt2  6144  ottpos  6448  dmtpos  6450  opiota  6494  riotaeqdv  6509  onoviun  6564  smoeq  6571  smoiso2  6590  tfr2b  6616  oarec  6764  oeeui  6804  nnacan  6830  nnmcan  6836  ereq1  6871  ereq2  6872  elecg  6902  ereldm  6907  ixpiin  7047  boxriin  7063  boxcutc  7064  omxpenlem  7168  nnsdomo  7260  enfi  7284  isfinite2  7324  ixpfi2  7363  elfi2  7377  fipwss  7392  ennum  7790  cardsdom2  7831  aleph11  7921  alephiso  7935  fin23lem26  8161  compssiso  8210  isf34lem4  8213  isfin5-2  8227  fin1a2lem5  8240  brdom7disj  8365  brdom6disj  8366  fpwwe2lem8  8468  fpwwe2lem12  8472  fpwwe2lem13  8473  genpass  8842  ltasr  8931  axpre-lttri  8996  infm3  9923  creur  9950  eqreznegel  10517  rpneg  10597  ltxr  10671  icoshftf1o  10976  elfzm11  11071  nn0ennn  11273  nnesq  11458  hashbclem  11656  hashf1lem1  11659  leiso  11663  fz1isolem  11665  rexfiuz  12106  cau4  12115  ello1mpt2  12271  o1lo1  12286  fsumcom2  12513  incexc2  12573  bitsmod  12903  bitscmp  12905  smueqlem  12957  hashdvds  13119  prmreclem2  13240  vdwapun  13297  vdwmc2  13302  imasaddfnlem  13708  comfeq  13887  oppcsect  13954  funcres2b  14049  funcpropd  14052  fullpropd  14072  fthpropd  14073  fthres2b  14082  fthres2c  14083  fullres2c  14091  ffthres2c  14092  fucsect  14124  fucinv  14125  setcsect  14199  tosso  14420  pospropd  14516  odulatb  14525  oduclatb  14526  isipodrs  14542  odudlatb  14577  mndpropd  14676  mhmpropd  14699  issubm2  14704  grppropd  14778  grpinvcnv  14814  conjghm  14991  conjnmzb  14995  ghmpropd  14998  gapm  15038  cmnpropd  15376  ablpropd  15377  eqgabl  15409  gsumcom2  15504  dmdprd  15514  dprdw  15523  subgdmdprd  15547  pgpfac1lem2  15588  pgpfac1lem4  15591  rngpropd  15650  crngpropd  15651  crngunit  15722  unitpropd  15757  isnirred  15760  drngpropd  15817  fldpropd  15818  subrgpropd  15857  rhmpropd  15858  abvpropd  15885  lmodprop2d  15961  lsspropd  16048  lmhmpropd  16100  lbspropd  16126  lvecprop2d  16193  lvecpropd  16194  rrgsupp  16306  opprdomn  16316  fiidomfld  16323  assapropd  16341  psrbagconf1o  16394  mplmonmul  16482  phlpropd  16841  eltopspOLD  16938  istps2OLD  16941  tpspropd  16960  tgss2  17007  lmbr2  17277  ist1-2  17365  ist1-3  17367  subislly  17497  iskgen3  17534  txcnmpt  17609  hausdiag  17630  hauseqlcld  17631  xkococnlem  17644  tgqtop  17697  txhmeo  17788  uffix2  17909  ufildr  17916  txflf  17991  tgphaus  18099  divstgplem  18103  divstgphaus  18105  xpsdsval  18364  blin  18404  blres  18414  xmeterval  18415  xmspropd  18456  mspropd  18457  setsms  18463  metequiv  18492  metustsymOLD  18544  metustsym  18545  restmetu  18570  ngppropd  18631  xrtgioo  18790  metdsge  18832  icopnfcnv  18920  iccpnfcnv  18922  lmhmclm  19064  lmmbr  19164  equivcmet  19221  cmspropd  19255  iunmbl2  19404  ioombl1lem4  19408  mbfaddlem  19505  i1fmullem  19539  itg1mulc  19549  iblcnlem1  19632  iblrelem  19635  iblre  19638  iblcn  19643  limcun  19735  mvth  19829  ofmulrt  20152  resinf1o  20391  quad2  20632  1cubr  20635  dcubic  20639  wilthlem2  20805  dvdsflip  20920  dvdsflf1o  20925  dvdsflsumcom  20926  fsumvma  20950  vmasum  20953  logfac2  20954  logfaclbnd  20959  dchrelbas3  20975  lgsquadlem1  21091  lgsquadlem2  21092  eupath2lem2  21653  isass  21857  ocin  22751  chpsscon3  22958  chscllem2  23093  adjval  23346  pjimai  23632  mdsldmd1i  23787  elat2  23796  mdsymi  23867  rmoxfrdOLD  23932  rmoxfrd  23933  disjrdx  23984  fmptcof2  24029  funcnv5mpt  24037  1stpreima  24048  2ndpreima  24049  zhmnrg  24304  qqhval2  24319  dfrtrclrec2  25096  fprodcom2  25261  dfpo2  25326  dfres3  25330  dfrdg4  25703  altopthbg  25717  ax5seg  25781  broutsideof3  25964  istotbnd3  26370  sstotbnd  26374  heibor  26420  isidlc  26515  smprngopr  26552  mrefg2  26651  jm2.23  26957  wepwsolem  27006  dnwech  27013  islssfg2  27037  gicabl  27131  islindf4  27176  pmtrfrn  27268  acsfn1p  27375  isdomn3  27391  ralbidar  27515  rexbidar  27516  sbcrel  27848  sbcfun  27854  dfateq12d  27860  aov0nbovbi  27926  fnotaovb  27929  elfzomelpfzo  27989  el2wlkonotot1  28071  2pthwlkonot  28082  usg2spot2nb  28168  bnj919  28842  bnj956  28853  bnj976  28854  bnj1366  28907  bnj916  29010  drex1NEW7  29200  drnf1NEW7  29201  drnf2wAUX7  29204  drnf2w2AUX7  29207  drnf2w3AUX7  29210  drsb1NEW7  29212  drnf2OLD7  29400  cbvexdOLD7  29419  sbal2OLD7  29453  islshpsm  29463  lcvexchlem1  29517  opcon1b  29681  isat3  29790  glbconN  29859  cdleme32fva  30919  cdlemg2cex  31073  dibelval3  31630  dib1dim  31648  doch11  31856  dochsordN  31857  mapdordlem1a  32117  mapd11  32122  mapdsord  32138  mapdcnv11N  32142  mapd0  32148

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178