Theorem 3bitr3g 313

Description: More general version of 3bitr3i 301. 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 285	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	bitrdi 287	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  notbid  318  cador  1610  cbvexdvaw  2041  cbvexdw  2344  cbvexd  2413  cbvrexdva  3219  raleq  3295  rexeqbidvvOLD  3309  cbvrexdva2  3321  rexeqf  3328  cbvexeqsetf  3457  dfsbcq2  3745  unineq  4242  iindif2  5034  reusv2  5350  rabxfrd  5364  opeqex  5454  eqbrrdv  5750  eqbrrdiv  5751  opelco2g  5824  opelcnvg  5837  ralrnmptw  7048  ralrnmpt  7050  fliftcnv  7267  eusvobj2  7360  br1steqg  7965  br2ndeqg  7966  ottpos  8188  smoiso  8304  ercnv  8667  ordiso2  9432  cantnfrescl  9597  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1  9610  cnfcom  9621  cnfcom3lem  9624  djulf1o  9836  djurf1o  9837  carden2  9911  cardeq0  10474  axpownd  10524  fpwwe2lem8  10561  fzen  13469  hasheq0  14298  incexc2  15773  divalglem4  16335  divalglem8  16339  divalgb  16343  sadadd  16406  sadass  16410  smuval2  16421  smumul  16432  isprm3  16622  vdwmc  16918  imasleval  17474  acsfn2  17598  invsym2  17699  yoniso  18220  pmtrfmvdn0  19403  dprd2d2  19987  cmpfi  23364  xkoinjcn  23643  tgpconncomp  24069  iscau3  25246  mbfimaopnlem  25624  ellimc3  25848  eldv  25867  eltayl  26335  atandm3  26856  noetasuplem4  27716  rmoxfrd  32579  opeldifid  32686  2ndpreima  32798  f1od2  32809  ordtconnlem1  34102  bnj1253  35193  usgrgt2cycl  35346  satfdm  35585  wl-dral1d  37786  wl-sb8eft  37806  wl-sb8et  37808  wl-equsb3  37811  wl-sb8eut  37833  wl-sb8eutv  37834  wl-issetft  37837  poimirlem2  37873  poimirlem16  37887  poimirlem18  37889  poimirlem21  37892  poimirlem22  37893  eqbrrdv2  39239  islpln5  39911  islvol5  39955  ntrneicls11  44446  radcnvrat  44670  trsbc  44896  iindif2f  45519  ichnreuop  47832  ichreuopeq  47833  pm5.32dav  49153  exp12bd  49155  reuxfr1dd  49166  aacllem  50160