Theorem 3bitr3g 316

Description: More general version of 3bitr3i 304. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)

Hypotheses

Ref	Expression
3bitr3g.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr3g.2	⊢ (𝜓 ↔ 𝜃)
3bitr3g.3	⊢ (𝜒 ↔ 𝜏)

Assertion

Ref	Expression
3bitr3g	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Proof of Theorem 3bitr3g

Step	Hyp	Ref	Expression
1		3bitr3g.2	. . 3 ⊢ (𝜓 ↔ 𝜃)
2		3bitr3g.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	bitr3id 288	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	syl6bb 290	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  notbid  321  cador  1610  cbvexdvaw  2046  cbvexdw  2348  cbvexd  2418  cbvrexdva2OLD  3405  vtoclgft  3501  dfsbcq2  3723  unineq  4204  iindif2  4962  reusv2  5269  rabxfrd  5283  opeqex  5353  eqbrrdv  5630  eqbrrdiv  5631  opelco2g  5702  opelcnvg  5715  ralrnmptw  6837  ralrnmpt  6839  fliftcnv  7043  eusvobj2  7128  br1steqg  7693  br2ndeqg  7694  ottpos  7885  smoiso  7982  ercnv  8293  ordiso2  8963  cantnfrescl  9123  cantnfp1lem3  9127  cantnflem1b  9133  cantnflem1  9136  cnfcom  9147  cnfcom3lem  9150  djulf1o  9325  djurf1o  9326  carden2  9400  cardeq0  9963  axpownd  10012  fpwwe2lem9  10049  fzen  12919  hasheq0  13720  incexc2  15185  divalglem4  15737  divalglem8  15741  divalgb  15745  sadadd  15806  sadass  15810  smuval2  15821  smumul  15832  isprm3  16017  vdwmc  16304  imasleval  16806  acsfn2  16926  invsym2  17025  yoniso  17527  pmtrfmvdn0  18582  dprd2d2  19159  cmpfi  22013  xkoinjcn  22292  tgpconncomp  22718  iscau3  23882  mbfimaopnlem  24259  ellimc3  24482  eldv  24501  eltayl  24955  atandm3  25464  rmoxfrd  30264  opeldifid  30362  2ndpreima  30467  f1od2  30483  ordtconnlem1  31277  bnj1253  32399  usgrgt2cycl  32490  satfdm  32729  noetalem3  33332  wl-dral1d  34936  wl-sb8et  34954  wl-equsb3  34957  wl-sb8eut  34978  wl-ax11-lem8  34989  wl-clelsb3df  35028  poimirlem2  35059  poimirlem16  35073  poimirlem18  35075  poimirlem21  35078  poimirlem22  35079  eqbrrdv2  36159  islpln5  36831  islvol5  36875  ntrneicls11  40793  radcnvrat  41018  trsbc  41246  ichnreuop  43989  ichreuopeq  43990  aacllem  45329