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  1609  cbvexdvaw  2040  cbvexdw  2343  cbvexd  2412  cbvrexdva  3217  raleq  3293  rexeqbidvvOLD  3307  cbvrexdva2  3319  rexeqf  3326  cbvexeqsetf  3455  dfsbcq2  3743  unineq  4240  iindif2  5032  reusv2  5348  rabxfrd  5362  opeqex  5446  eqbrrdv  5742  eqbrrdiv  5743  opelco2g  5816  opelcnvg  5829  ralrnmptw  7039  ralrnmpt  7041  fliftcnv  7257  eusvobj2  7350  br1steqg  7955  br2ndeqg  7956  ottpos  8178  smoiso  8294  ercnv  8656  ordiso2  9420  cantnfrescl  9585  cantnfp1lem3  9589  cantnflem1b  9595  cantnflem1  9598  cnfcom  9609  cnfcom3lem  9612  djulf1o  9824  djurf1o  9825  carden2  9899  cardeq0  10462  axpownd  10512  fpwwe2lem8  10549  fzen  13457  hasheq0  14286  incexc2  15761  divalglem4  16323  divalglem8  16327  divalgb  16331  sadadd  16394  sadass  16398  smuval2  16409  smumul  16420  isprm3  16610  vdwmc  16906  imasleval  17462  acsfn2  17586  invsym2  17687  yoniso  18208  pmtrfmvdn0  19391  dprd2d2  19975  cmpfi  23352  xkoinjcn  23631  tgpconncomp  24057  iscau3  25234  mbfimaopnlem  25612  ellimc3  25836  eldv  25855  eltayl  26323  atandm3  26844  noetasuplem4  27704  rmoxfrd  32567  opeldifid  32674  2ndpreima  32787  f1od2  32798  ordtconnlem1  34081  bnj1253  35173  usgrgt2cycl  35324  satfdm  35563  wl-dral1d  37736  wl-sb8eft  37756  wl-sb8et  37758  wl-equsb3  37761  wl-sb8eut  37783  wl-sb8eutv  37784  wl-issetft  37787  poimirlem2  37823  poimirlem16  37837  poimirlem18  37839  poimirlem21  37842  poimirlem22  37843  eqbrrdv2  39123  islpln5  39795  islvol5  39839  ntrneicls11  44331  radcnvrat  44555  trsbc  44781  iindif2f  45404  ichnreuop  47718  ichreuopeq  47719  pm5.32dav  49039  exp12bd  49041  reuxfr1dd  49052  aacllem  50046