Theorem 3bitr3g 287

Description: More general version of 3bitr3i 275. 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 259	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3g.3	. 2 |- ( ch <-> ta )
5	3, 4	syl6bb 261	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:  notbid  292  cador  1461  equequ2  1804  dfsbcq2  3327  unineq  3745  iindif2  4384  reusv2  4643  rabxfrd  4658  opeqex  4727  eqbrrdv  5088  eqbrrdiv  5089  opelco2g  5159  opelcnvg  5171  ralrnmpt  6016  fliftcnv  6184  eusvobj2  6263  ottpos  6957  smoiso  7025  ercnv  7324  ordiso2  7932  cantnfrescl  8086  cantnfp1lem3  8090  cantnflem1b  8096  cantnflem1  8099  cantnfp1lem3OLD  8116  cantnflem1bOLD  8119  cantnflem1OLD  8122  cnfcom  8135  cnfcom3lem  8138  cnfcomOLD  8143  cnfcom3lemOLD  8146  carden2  8359  cardeq0  8918  axpownd  8967  fpwwe2lem9  9005  fzen  11706  hasheq0  12419  incexc2  13735  divalglem4  14141  divalglem8  14145  divalgb  14149  divalgmod  14151  sadadd  14204  sadass  14208  smuval2  14219  smumul  14230  isprm3  14313  vdwmc  14583  imasleval  15033  acsfn2  15155  invsym2  15254  yoniso  15756  pmtrfmvdn0  16689  dprd2d2  17291  cmpfi  20078  xkoinjcn  20357  tgpconcomp  20780  iscau3  21886  mbfimaopnlem  22231  ellimc3  22452  eldv  22471  eltayl  22924  atandm3  23409  el2wlkonot  25074  el2spthonot  25075  rmoxfrdOLD  27592  rmoxfrd  27593  opeldifid  27673  2ndpreima  27757  f1od2  27781  ordtconlem1  28144  wl-dral1d  30227  wl-sb8et  30244  wl-equsb3  30247  wl-sb8eut  30265  wl-ax11-lem8  30275  eqbrrdv2  30847  radcnvrat  31439  aacllem  33623  trsbc  33720  bnj1253  34493  islpln5  35675  islvol5  35719