Theorem 3bitr3g 290

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

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

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 188

This theorem is referenced by:  notbid  295  cador  1504  equequ2  1853  dfsbcq2  3245  unineq  3666  iindif2  4311  reusv2  4573  rabxfrd  4585  opeqex  4654  eqbrrdv  4894  eqbrrdiv  4895  opelco2g  4964  opelcnvg  4976  ralrnmpt  5990  fliftcnv  6163  eusvobj2  6242  ottpos  6938  smoiso  7036  ercnv  7339  ordiso2  7983  cantnfrescl  8133  cantnfp1lem3  8137  cantnflem1b  8143  cantnflem1  8146  cnfcom  8157  cnfcom3lem  8160  carden2  8373  cardeq0  8928  axpownd  8977  fpwwe2lem9  9014  fzen  11767  hasheq0  12494  incexc2  13839  divalglem4  14318  divalglem8  14323  divalgb  14328  divalgmod  14330  sadadd  14384  sadass  14388  smuval2  14399  smumul  14410  isprm3  14576  vdwmc  14871  imasleval  15390  acsfn2  15512  invsym2  15611  yoniso  16113  pmtrfmvdn0  17046  dprd2d2  17620  cmpfi  20365  xkoinjcn  20644  tgpconcomp  21069  iscau3  22190  mbfimaopnlem  22553  ellimc3  22776  eldv  22795  eltayl  23257  atandm3  23746  el2wlkonot  25539  el2spthonot  25540  rmoxfrdOLD  28070  rmoxfrd  28071  opeldifid  28156  2ndpreima  28234  f1od2  28259  ordtconlem1  28682  bnj1253  29778  wl-dral1d  31771  wl-sb8et  31788  wl-equsb3  31791  wl-sb8eut  31813  wl-ax11-lem8  31829  poimirlem2  31849  poimirlem16  31863  poimirlem18  31865  poimirlem21  31868  poimirlem22  31869  eqbrrdv2  32346  islpln5  33012  islvol5  33056  radcnvrat  36576  trsbc  36814  aacllem  40143