Theorem 3bitr3g 315

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  notbid  320  cador  1627  cbvexdvaw  2058  cbvexdw  2369  cbvexd  2438  cbvrexdva  3242  raleq  3316  cbvrexdva2  3338  rexeqf  3343  cbvexeqsetf  3468  dfsbcq2  3745  unineq  4238  iindif2  5031  reusv2  5357  rabxfrd  5371  opeqex  5464  eqbrrdv  5761  eqbrrdiv  5762  opelco2g  5835  opelcnvg  5848  ralrnmptw  7070  ralrnmpt  7072  fliftcnv  7290  eusvobj2  7383  br1steqg  7987  br2ndeqg  7988  ottpos  8210  smoiso  8327  ercnv  8694  ordiso2  9457  cantnfrescl  9625  cantnfp1lem3  9629  cantnflem1b  9635  cantnflem1  9638  cnfcom  9649  cnfcom3lem  9652  djulf1o  9864  djurf1o  9865  carden2  9939  cardeq0  10503  axpownd  10553  fpwwe2lem8  10590  fzen  13540  hasheq0  14370  incexc2  15859  divalglem4  16421  divalglem8  16425  divalgb  16429  sadadd  16492  sadass  16496  smuval2  16507  smumul  16518  isprm3  16708  vdwmc  17005  imasleval  17562  acsfn2  17686  invsym2  17787  yoniso  18308  pmtrfmvdn0  19493  dprd2d2  20077  cmpfi  23456  xkoinjcn  23735  tgpconncomp  24161  iscau3  25328  mbfimaopnlem  25705  ellimc3  25929  eldv  25948  eltayl  26411  atandm3  26931  noetasuplem4  27788  rmoxfrd  32651  opeldifid  32759  2ndpreima  32871  f1od2  32882  ordtconnlem1  34182  bnj1253  35273  usgrgt2cycl  35441  satfdm  35680  wl-dral1d  37995  wl-sb8eft  38015  wl-sb8et  38017  wl-equsb3  38020  wl-sb8eut  38042  wl-sb8eutv  38043  wl-issetft  38046  poimirlem2  38082  poimirlem16  38096  poimirlem18  38098  poimirlem21  38101  poimirlem22  38102  eqbrrdv2  39448  islpln5  40120  islvol5  40164  ntrneicls11  44627  radcnvrat  44851  trsbc  45077  iindif2f  45699  ichnreuop  48039  ichreuopeq  48040  pm5.32dav  49376  exp12bd  49378  reuxfr1dd  49389  aacllem  50383