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  2343  cbvexd  2412  cbvrexdva  3218  raleq  3292  cbvrexdva2  3314  rexeqf  3319  cbvexeqsetf  3444  dfsbcq2  3731  unineq  4228  iindif2  5019  reusv2  5345  rabxfrd  5359  opeqex  5452  eqbrrdv  5749  eqbrrdiv  5750  opelco2g  5822  opelcnvg  5835  ralrnmptw  7046  ralrnmpt  7048  fliftcnv  7266  eusvobj2  7359  br1steqg  7964  br2ndeqg  7965  ottpos  8186  smoiso  8302  ercnv  8665  ordiso2  9430  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  13495  hasheq0  14325  incexc2  15803  divalglem4  16365  divalglem8  16369  divalgb  16373  sadadd  16436  sadass  16440  smuval2  16451  smumul  16462  isprm3  16652  vdwmc  16949  imasleval  17505  acsfn2  17629  invsym2  17730  yoniso  18251  pmtrfmvdn0  19437  dprd2d2  20021  cmpfi  23373  xkoinjcn  23652  tgpconncomp  24078  iscau3  25245  mbfimaopnlem  25622  ellimc3  25846  eldv  25865  eltayl  26325  atandm3  26842  noetasuplem4  27700  rmoxfrd  32562  opeldifid  32669  2ndpreima  32781  f1od2  32792  ordtconnlem1  34068  bnj1253  35159  usgrgt2cycl  35312  satfdm  35551  wl-dral1d  37856  wl-sb8eft  37876  wl-sb8et  37878  wl-equsb3  37881  wl-sb8eut  37903  wl-sb8eutv  37904  wl-issetft  37907  poimirlem2  37943  poimirlem16  37957  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  eqbrrdv2  39309  islpln5  39981  islvol5  40025  ntrneicls11  44517  radcnvrat  44741  trsbc  44967  iindif2f  45590  ichnreuop  47932  ichreuopeq  47933  pm5.32dav  49269  exp12bd  49271  reuxfr1dd  49282  aacllem  50276