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  1506  equequ2  1851  dfsbcq2  3308  unineq  3729  iindif2  4371  reusv2  4631  rabxfrd  4643  opeqex  4712  eqbrrdv  4952  eqbrrdiv  4953  opelco2g  5022  opelcnvg  5034  ralrnmpt  6046  fliftcnv  6219  eusvobj2  6298  ottpos  6991  smoiso  7089  ercnv  7392  ordiso2  8030  cantnfrescl  8180  cantnfp1lem3  8184  cantnflem1b  8190  cantnflem1  8193  cnfcom  8204  cnfcom3lem  8207  carden2  8420  cardeq0  8975  axpownd  9024  fpwwe2lem9  9062  fzen  11814  hasheq0  12541  incexc2  13874  divalglem4  14352  divalglem8  14356  divalgb  14360  divalgmod  14362  sadadd  14415  sadass  14419  smuval2  14430  smumul  14441  isprm3  14604  vdwmc  14891  imasleval  15398  acsfn2  15520  invsym2  15619  yoniso  16121  pmtrfmvdn0  17054  dprd2d2  17612  cmpfi  20354  xkoinjcn  20633  tgpconcomp  21058  iscau3  22141  mbfimaopnlem  22488  ellimc3  22711  eldv  22730  eltayl  23180  atandm3  23669  el2wlkonot  25442  el2spthonot  25443  rmoxfrdOLD  27963  rmoxfrd  27964  opeldifid  28049  2ndpreima  28128  f1od2  28152  ordtconlem1  28569  bnj1253  29614  wl-dral1d  31571  wl-sb8et  31588  wl-equsb3  31591  wl-sb8eut  31609  wl-ax11-lem8  31625  poimirlem2  31645  poimirlem16  31659  poimirlem18  31661  poimirlem21  31664  poimirlem22  31665  eqbrrdv2  32142  islpln5  32808  islvol5  32852  radcnvrat  36299  trsbc  36537  aacllem  39300