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 205

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 206

This theorem is referenced by:  notbid  318  cador  1614  cbvexdvaw  2046  cbvexdw  2340  cbvexd  2410  rexeqbidvv  3338  vtoclgft  3491  dfsbcq2  3723  unineq  4217  iindif2  5011  reusv2  5330  rabxfrd  5344  opeqex  5416  eqbrrdv  5702  eqbrrdiv  5703  opelco2g  5775  opelcnvg  5788  ralrnmptw  6967  ralrnmpt  6969  fliftcnv  7178  eusvobj2  7264  br1steqg  7846  br2ndeqg  7847  ottpos  8043  smoiso  8184  ercnv  8502  ordiso2  9252  cantnfrescl  9412  cantnfp1lem3  9416  cantnflem1b  9422  cantnflem1  9425  cnfcom  9436  cnfcom3lem  9439  djulf1o  9671  djurf1o  9672  carden2  9746  cardeq0  10309  axpownd  10358  fpwwe2lem8  10395  fzen  13272  hasheq0  14076  incexc2  15548  divalglem4  16103  divalglem8  16107  divalgb  16111  sadadd  16172  sadass  16176  smuval2  16187  smumul  16198  isprm3  16386  vdwmc  16677  imasleval  17250  acsfn2  17370  invsym2  17473  yoniso  18001  pmtrfmvdn0  19068  dprd2d2  19645  cmpfi  22557  xkoinjcn  22836  tgpconncomp  23262  iscau3  24440  mbfimaopnlem  24817  ellimc3  25041  eldv  25060  eltayl  25517  atandm3  26026  rmoxfrd  30837  opeldifid  30934  2ndpreima  31036  f1od2  31052  ordtconnlem1  31870  bnj1253  32993  usgrgt2cycl  33088  satfdm  33327  noetasuplem4  33935  wl-dral1d  35686  wl-sb8et  35704  wl-equsb3  35707  wl-sb8eut  35728  wl-ax11-lem8  35739  poimirlem2  35775  poimirlem16  35789  poimirlem18  35791  poimirlem21  35794  poimirlem22  35795  eqbrrdv2  36873  islpln5  37545  islvol5  37589  ntrneicls11  41670  radcnvrat  41902  trsbc  42130  ichnreuop  44893  ichreuopeq  44894  pm5.32dav  46108  exp12bd  46110  aacllem  46474