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  1446  equequ2  1785  dfsbcq2  3316  unineq  3733  iindif2  4384  reusv2  4643  rabxfrd  4658  opeqex  4728  eqbrrdv  5090  eqbrrdiv  5091  opelco2g  5160  opelcnvg  5172  ralrnmpt  6025  fliftcnv  6194  eusvobj2  6274  ottpos  6967  smoiso  7035  ercnv  7334  ordiso2  7943  cantnfrescl  8098  cantnfp1lem3  8102  cantnflem1b  8108  cantnflem1  8111  cantnfp1lem3OLD  8128  cantnflem1bOLD  8131  cantnflem1OLD  8134  cnfcom  8147  cnfcom3lem  8150  cnfcomOLD  8155  cnfcom3lemOLD  8158  carden2  8371  cardeq0  8930  axpownd  8981  fpwwe2lem9  9019  fzen  11713  hasheq0  12414  incexc2  13631  divalglem4  14035  divalglem8  14039  divalgb  14043  divalgmod  14045  sadadd  14098  sadass  14102  smuval2  14113  smumul  14124  isprm3  14207  vdwmc  14477  imasleval  14919  acsfn2  15041  invsym2  15138  yoniso  15532  pmtrfmvdn0  16465  dprd2d2  17071  cmpfi  19885  xkoinjcn  20165  tgpconcomp  20588  iscau3  21694  mbfimaopnlem  22039  ellimc3  22260  eldv  22279  eltayl  22731  atandm3  23185  el2wlkonot  24845  el2spthonot  24846  rmoxfrdOLD  27367  rmoxfrd  27368  opeldifid  27432  2ndpreima  27501  f1od2  27523  ordtconlem1  27883  wl-dral1d  29959  wl-sb8et  29976  wl-equsb3  29979  wl-sb8eut  29997  wl-ax11-lem8  30007  eqbrrdv2  30579  radcnvrat  31171  trsbc  33044  bnj1253  33806  islpln5  34999  islvol5  35043