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  1299  3anbi123d  1300  nanbi1  1355  nanbi2  1356  xorbi12d  1378  hadbi123d  1437  cadbi123d  1438  cad1  1453  had0  1458  nfbidf  1873  cbvexd  2012  drex1  2055  drnf1  2057  drsb1  2104  eujustALT  2271  eubid  2288  mobid  2289  eqeq1d  2445  eqeq1dALT  2446  eqeq1OLD  2448  eqeq2d  2457  eqeq2OLD  2459  eleq1d  2512  eleq2d  2513  eleq2dALT  2514  eleq1OLD  2517  eleq2OLD  2518  nfceqdf  2600  drnfc1  2624  drnfc2  2625  neeq1OLD  2725  neeq2OLD  2727  neleq12d  2780  neleq1OLD  2782  neleq2OLD  2784  r19.21t  2840  r19.21tOLD  2841  ralbida  2876  ralbidv2  2878  r19.23t  2921  rexbida  2949  rexbidv2  2950  ralcom2  3008  reubida  3026  rmobida  3031  raleqf  3036  rexeqf  3037  reueq1f  3038  rmoeq1f  3039  cbvraldva2  3074  cbvrexdva2  3075  dfsbcq  3315  sbceqbid  3320  sbcbi2  3364  sbcbid  3371  sbcrextOLD  3395  sbcrext  3396  sbcabel  3402  psseq1  3576  psseq2  3577  ssconb  3622  uneq1  3636  ineq1  3678  difin2  3745  reuun2  3766  sbcnel12g  3812  sbnfc2  3840  reldisj  3856  undif4  3869  disjssun  3870  pssdifcom1  3899  pssdifcom2  3900  sbcssg  3925  eltpg  4056  raltpg  4065  rextpg  4066  r19.12sn  4080  intmin4  4301  dfiun2g  4347  iindif2  4384  iinin2  4385  disjprg  4433  disjxun  4435  breq  4439  breq1  4440  breq2  4441  treq  4536  reusv2lem5  4642  reusv5OLD  4647  reusv7OLD  4649  rexxfrd  4652  rexxfr2d  4654  rabxfrd  4658  opthg2  4714  oteqex2  4729  oteqex  4730  poeq1  4793  soeq1  4809  freq1  4839  weeq1  4857  weeq2  4858  ordeq  4875  limeq  4880  ordunisssuc  4970  opthprc  5037  wesn  5061  releq  5075  sbcrel  5079  eqrel  5082  eqrelrel  5094  xpiindi  5128  brcnvg  5173  brresg  5272  resieq  5274  dmsnopg  5469  dfco2a  5497  iotaeq  5549  sniota  5568  sbcfung  5601  imadif  5653  fneq1  5659  fneq2  5660  feq1  5703  feq2  5704  feq3  5705  sbcfng  5718  sbcfg  5719  f1eq1  5766  f1eq2  5767  f1eq3  5768  foeq1  5781  foeq2  5782  foeq3  5783  f1oeq1  5797  f1oeq2  5798  f1oeq3  5799  mpteqb  5955  rexrnmpt  6026  dffo3  6031  fmptco  6049  dff13  6151  f1imaeq  6158  f1imapss  6159  cbvexfo  6178  f1eqcocnv  6189  fliftcnv  6194  isoeq1  6200  isoeq2  6201  isoeq3  6202  isoeq4  6203  isoeq5  6204  isomin  6218  isowe  6230  fnotovb  6323  mpt2eq123  6341  rexrnmpt2  6403  iunpw  6599  tfinds  6679  fun11iun  6745  opiota  6844  ottpos  6967  dmtpos  6969  onoviun  7016  smoeq  7023  smoiso2  7042  tfr2b  7067  oarec  7213  oeeui  7253  nnacan  7279  nnmcan  7285  ereq1  7320  ereq2  7321  elecg  7352  ereldm  7357  ixpiin  7497  boxriin  7513  boxcutc  7514  omxpenlem  7620  nnsdomo  7714  enfi  7738  isfinite2  7780  ixpfi2  7820  elfi2  7876  fipwss  7891  ennum  8331  cardsdom2  8372  aleph11  8468  alephiso  8482  fin23lem26  8708  compssiso  8757  isf34lem4  8760  isfin5-2  8774  fin1a2lem5  8787  brdom7disj  8912  brdom6disj  8913  fpwwe2lem8  9018  fpwwe2lem12  9022  fpwwe2lem13  9023  genpass  9390  ltasr  9480  axpre-lttri  9545  infm3  10508  creur  10536  eqreznegel  11176  rpneg  11258  ltxr  11333  icoshftf1o  11652  elfzm11  11758  elfzomelpfzo  11893  nn0ennn  12068  nnesq  12269  hashbclem  12480  hashf1lem1  12483  leiso  12487  fz1isolem  12489  pr2pwpr  12499  repsdf2  12729  rexfiuz  13159  cau4  13168  ello1mpt2  13324  o1lo1  13339  fsumcom2  13568  incexc2  13629  bitsmod  13963  bitscmp  13965  smueqlem  14017  hashdvds  14182  prmreclem2  14312  vdwapun  14369  vdwmc2  14374  imasaddfnlem  14802  comfeq  14978  oppcsect  15045  funcres2b  15140  funcpropd  15143  fullpropd  15163  fthpropd  15164  fthres2b  15173  fthres2c  15174  fullres2c  15182  ffthres2c  15183  fucsect  15215  fucinv  15216  setcsect  15290  tosso  15540  pospropd  15638  odulatb  15647  oduclatb  15648  isipodrs  15665  odudlatb  15700  issgrpv  15787  issgrpn0  15788  mndpropd  15820  mhmpropd  15846  issubm2  15853  grppropd  15942  grpinvcnv  15980  conjghm  16171  conjnmzb  16175  ghmpropd  16178  gapm  16218  symg1bas  16295  pmtrfrn  16357  cmnpropd  16681  ablpropd  16682  eqgabl  16717  gsumcom2  16877  dmdprd  16903  dprdw  16917  dprdwOLD  16924  subgdmdprd  16955  pgpfac1lem2  17000  pgpfac1lem4  17003  ringpropd  17104  crngpropd  17105  crngunit  17185  unitpropd  17220  isnirred  17223  drngpropd  17297  fldpropd  17298  subrgpropd  17337  rhmpropd  17338  abvpropd  17365  lmodprop2d  17446  lsspropd  17537  lmhmpropd  17593  lbspropd  17619  lvecprop2d  17686  lvecpropd  17687  rrgsuppOLD  17814  opprdomn  17824  fiidomfld  17831  assapropd  17850  psrbagconf1o  17900  mplmonmul  18000  phlpropd  18563  mat1dimbas  18847  eltopspOLD  19292  istps2OLD  19295  tpspropd  19314  tgss2  19362  lmbr2  19633  ist1-2  19721  ist1-3  19723  subislly  19855  dissnlocfin  19903  iskgen3  19923  txcnmpt  19998  hausdiag  20019  hauseqlcld  20020  xkococnlem  20033  tgqtop  20086  txhmeo  20177  uffix2  20298  ufildr  20305  txflf  20380  tgphaus  20488  qustgplem  20492  qustgphaus  20494  xpsdsval  20757  blin  20797  blres  20807  xmeterval  20808  xmspropd  20849  mspropd  20850  setsms  20856  metequiv  20885  metustsymOLD  20937  metustsym  20938  restmetu  20963  ngppropd  21024  xrtgioo  21184  metdsge  21226  icopnfcnv  21315  iccpnfcnv  21317  lmhmclm  21459  lmmbr  21570  equivcmet  21627  cmspropd  21661  iunmbl2  21840  ioombl1lem4  21844  mbfaddlem  21940  i1fmullem  21974  itg1mulc  21984  iblcnlem1  22067  iblrelem  22070  iblre  22073  iblcn  22078  limcun  22172  mvth  22266  ofmulrt  22550  resinf1o  22795  quad2  23042  1cubr  23045  dcubic  23049  wilthlem2  23215  dvdsflip  23330  dvdsflf1o  23335  dvdsflsumcom  23336  fsumvma  23360  vmasum  23363  logfac2  23364  logfaclbnd  23369  dchrelbas3  23385  lgsquadlem1  23501  lgsquadlem2  23502  ax5seg  24113  clwwlknscsh  24691  el2wlkonotot1  24746  2pthwlkonot  24757  rusgranumwlkb0  24825  eupath2lem2  24850  usg2spot2nb  24937  numclwwlkovfel2  24955  isass  25190  ocin  26086  chpsscon3  26293  chscllem2  26428  adjval  26681  pjimai  26967  mdsldmd1i  27122  elat2  27131  mdsymi  27202  sbceqbidf  27252  rmoxfrdOLD  27263  rmoxfrd  27264  disjrdx  27322  eqrelrd2  27339  fmptcof2  27374  ofpreima  27379  funcnv5mpt  27383  1stpreima  27396  2ndpreima  27397  fpwrelmapffslem  27427  locfinreflem  27716  zhmnrg  27821  qqhval2  27836  ismntop  27877  dfrtrclrec2  28939  fprodcom2  29089  dfpo2  29159  dfres3  29163  sscoid  29538  dfrdg4  29575  altopthbg  29593  broutsideof3  29751  wl-sb8eut  29997  wl-sb8mot  29998  ftc1anclem5  30069  istotbnd3  30242  sstotbnd  30246  heibor  30292  isidlc  30387  smprngopr  30424  mrefg2  30614  jm2.23  30913  wepwsolem  30962  dnwech  30969  islssfg2  30992  gicabl  31022  acsfn1p  31124  isdomn3  31140  ralbidar  31308  rexbidar  31309  iccintsng  31499  dfateq12d  32052  aov0nbovbi  32118  fnotaovb  32121  rexxfrd2  32142  mgmhmpropd  32311  rngcsect  32528  rngcsectOLD  32540  ringcsect  32576  ringcsectOLD  32600  lindslinindsimp2lem5  32798  trsbc  33044  bnj919  33558  bnj956  33568  bnj976  33569  bnj1366  33621  bnj916  33724  bj-nfbi  33965  bj-cbvexdv  34049  bj-drex1v  34075  bj-drnf1v  34076  bj-eleq1w  34170  bj-eleq2w  34171  islshpsm  34445  lcvexchlem1  34499  opcon1b  34663  isat3  34772  glbconN  34841  cdleme32fva  35903  cdlemg2cex  36057  dibelval3  36614  dib1dim  36632  doch11  36840  dochsordN  36841  mapdordlem1a  37101  mapd11  37106  mapdsord  37122  mapdcnv11N  37126  mapd0  37132  pwinfig  37449  heeq12  37487