Theorem 3bitr3g 279

Description: More general version of 3bitr3i 267. 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 251	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3g.3	. 2 |- ( ch <-> ta )
5	3, 4	syl6bb 253	1 |- ( ph -> ( th <-> ta ) )

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

This theorem is referenced by:  notbid  286  cador  1397  equequ2  1694  dfsbcq2  3124  unineq  3551  iindif2  4120  opeqex  4407  reusv2  4688  rabxfrd  4703  eqbrrdv  4932  eqbrrdiv  4933  opelco2g  4999  opelcnvg  5011  ralrnmpt  5837  fliftcnv  5992  ottpos  6448  eusvobj2  6541  smoiso  6583  ercnv  6885  ordiso2  7440  cantnfrescl  7588  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1  7601  cnfcom  7613  cnfcom3lem  7616  carden2  7830  cardeq0  8383  axpownd  8432  fpwwe2lem9  8469  fzen  11028  hasheq0  11599  incexc2  12573  divalglem4  12871  divalglem8  12875  divalgb  12879  divalgmod  12881  sadadd  12934  sadass  12938  smuval2  12949  smumul  12960  isprm3  13043  vdwmc  13301  imasleval  13721  acsfn2  13843  invsym2  13943  yoniso  14337  dprd2d2  15557  cmpfi  17425  xkoinjcn  17672  tgpconcomp  18095  iscau3  19184  mbfimaopnlem  19500  ellimc3  19719  eldv  19738  eltayl  20229  atandm3  20671  rmoxfrdOLD  23932  rmoxfrd  23933  2ndpreima  24049  wl-bibi2d  26130  eqbrrdv2  26602  pmtrfmvdn0  27271  el2wlkonot  28066  el2spthonot  28067  bnj1253  29092  islpln5  30017  islvol5  30061

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