Theorem 3bitr3g 295

Description: More general version of 3bitr3i 283. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)

Hypotheses

Ref	Expression
3bitr3g.1	|- ( ph -> ( ps <-> ch ) )
3bitr3g.2	|- ( ps <-> th )
3bitr3g.3	|- ( ch <-> ta )

Assertion

Ref	Expression
3bitr3g	|- ( ph -> ( th <-> ta ) )

Proof of Theorem 3bitr3g

Step	Hyp	Ref	Expression
1		3bitr3g.2	. . 3 |- ( ps <-> th )
2		3bitr3g.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3	1, 2	syl5bbr 267	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3g.3	. 2 |- ( ch <-> ta )
5	3, 4	syl6bb 269	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:  notbid  300  cador  1521  equequ2  1878  dfsbcq2  3281  unineq  3704  iindif2  4360  reusv2  4622  rabxfrd  4634  opeqex  4705  eqbrrdv  4950  eqbrrdiv  4951  opelco2g  5020  opelcnvg  5032  ralrnmpt  6053  fliftcnv  6228  eusvobj2  6307  ottpos  7008  smoiso  7106  ercnv  7409  ordiso2  8055  cantnfrescl  8206  cantnfp1lem3  8210  cantnflem1b  8216  cantnflem1  8219  cnfcom  8230  cnfcom3lem  8233  carden2  8446  cardeq0  9002  axpownd  9051  fpwwe2lem9  9088  fzen  11844  hasheq0  12575  incexc2  13944  divalglem4  14423  divalglem8  14428  divalgb  14433  divalgmod  14435  sadadd  14489  sadass  14493  smuval2  14504  smumul  14515  isprm3  14681  vdwmc  14976  imasleval  15495  acsfn2  15617  invsym2  15716  yoniso  16218  pmtrfmvdn0  17151  dprd2d2  17725  cmpfi  20471  xkoinjcn  20750  tgpconcomp  21175  iscau3  22296  mbfimaopnlem  22659  ellimc3  22882  eldv  22901  eltayl  23363  atandm3  23852  el2wlkonot  25645  el2spthonot  25646  rmoxfrdOLD  28176  rmoxfrd  28177  opeldifid  28258  2ndpreima  28336  f1od2  28357  ordtconlem1  28778  bnj1253  29874  wl-dral1d  31908  wl-sb8et  31925  wl-equsb3  31928  wl-sb8eut  31950  wl-ax11-lem8  31966  poimirlem2  31986  poimirlem16  32000  poimirlem18  32002  poimirlem21  32005  poimirlem22  32006  eqbrrdv2  32479  islpln5  33144  islvol5  33188  radcnvrat  36706  trsbc  36944  aacllem  40812