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  1442  equequ2  1748  dfsbcq2  3334  unineq  3748  iindif2  4394  reusv2  4653  rabxfrd  4668  opeqex  4738  eqbrrdv  5100  eqbrrdiv  5101  opelco2g  5170  opelcnvg  5182  ralrnmpt  6030  fliftcnv  6197  eusvobj2  6277  ottpos  6965  smoiso  7033  ercnv  7332  ordiso2  7940  cantnfrescl  8095  cantnfp1lem3  8099  cantnflem1b  8105  cantnflem1  8108  cantnfp1lem3OLD  8125  cantnflem1bOLD  8128  cantnflem1OLD  8131  cnfcom  8144  cnfcom3lem  8147  cnfcomOLD  8152  cnfcom3lemOLD  8155  carden2  8368  cardeq0  8927  axpownd  8978  fpwwe2lem9  9016  fzen  11703  hasheq0  12401  incexc2  13613  divalglem4  13913  divalglem8  13917  divalgb  13921  divalgmod  13923  sadadd  13976  sadass  13980  smuval2  13991  smumul  14002  isprm3  14085  vdwmc  14355  imasleval  14796  acsfn2  14918  invsym2  15018  yoniso  15412  pmtrfmvdn0  16293  dprd2d2  16895  cmpfi  19702  xkoinjcn  19951  tgpconcomp  20374  iscau3  21480  mbfimaopnlem  21825  ellimc3  22046  eldv  22065  eltayl  22517  atandm3  22965  el2wlkonot  24573  el2spthonot  24574  rmoxfrdOLD  27095  rmoxfrd  27096  opeldifid  27157  2ndpreima  27225  f1od2  27247  ordtconlem1  27570  wl-dral1d  29589  wl-sb8et  29606  wl-equsb3  29609  wl-sb8eut  29627  wl-ax11-lem8  29637  eqbrrdv2  30236  trsbc  32409  bnj1253  33170  islpln5  34349  islvol5  34393