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  294  cador  1432  equequ2  1737  dfsbcq2  3189  unineq  3600  iindif2  4239  reusv2  4498  rabxfrd  4513  opeqex  4582  eqbrrdv  4937  eqbrrdiv  4938  opelco2g  5007  opelcnvg  5019  ralrnmpt  5852  fliftcnv  6004  eusvobj2  6084  ottpos  6755  smoiso  6823  ercnv  7122  ordiso2  7729  cantnfrescl  7884  cantnfp1lem3  7888  cantnflem1b  7894  cantnflem1  7897  cantnfp1lem3OLD  7914  cantnflem1bOLD  7917  cantnflem1OLD  7920  cnfcom  7933  cnfcom3lem  7936  cnfcomOLD  7941  cnfcom3lemOLD  7944  carden2  8157  cardeq0  8716  axpownd  8767  fpwwe2lem9  8805  fzen  11467  hasheq0  12131  incexc2  13301  divalglem4  13600  divalglem8  13604  divalgb  13608  divalgmod  13610  sadadd  13663  sadass  13667  smuval2  13678  smumul  13689  isprm3  13772  vdwmc  14039  imasleval  14479  acsfn2  14601  invsym2  14701  yoniso  15095  pmtrfmvdn0  15968  dprd2d2  16543  cmpfi  19011  xkoinjcn  19260  tgpconcomp  19683  iscau3  20789  mbfimaopnlem  21133  ellimc3  21354  eldv  21373  eltayl  21825  atandm3  22273  rmoxfrdOLD  25876  rmoxfrd  25877  2ndpreima  26002  f1od2  26024  ordtconlem1  26354  wl-dral1d  28360  wl-sb8et  28377  wl-equsb3  28380  wl-sb8eut  28398  wl-ax11-lem8  28408  eqbrrdv2  29008  el2wlkonot  30388  el2spthonot  30389  trsbc  31247  bnj1253  32008  islpln5  33179  islvol5  33223