Theorem 3bitr3g 316

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  notbid  321  cador  1641  cbvexdvaw  2072  cbvexdw  2373  cbvexd  2442  cbvrexdva  3248  raleq  3322  cbvrexdva2  3343  rexeqf  3348  cbvexeqsetf  3472  dfsbcq2  3749  unineq  4241  iindif2  5045  reusv2  5376  rabxfrd  5390  opeqex  5483  eqbrrdv  5781  eqbrrdiv  5782  opelco2g  5855  opelcnvg  5868  ralrnmptw  7093  ralrnmpt  7095  fliftcnv  7315  eusvobj2  7408  br1steqg  8010  br2ndeqg  8011  ottpos  8234  smoiso  8351  ercnv  8718  ordiso2  9480  cantnfrescl  9648  cantnfp1lem3  9652  cantnflem1b  9658  cantnflem1  9661  cnfcom  9672  cnfcom3lem  9675  djulf1o  9910  djurf1o  9911  carden2  9985  cardeq0  10547  axpownd  10597  fpwwe2lem8  10634  fzen  13581  hasheq0  14413  incexc2  15911  divalglem4  16472  divalglem8  16476  divalgb  16480  sadadd  16543  sadass  16547  smuval2  16558  smumul  16569  isprm3  16759  vdwmc  17056  imasleval  17613  acsfn2  17737  invsym2  17838  yoniso  18359  pmtrfmvdn0  19556  dprd2d2  20140  cmpfi  23595  xkoinjcn  23875  tgpconncomp  24301  iscau3  25468  mbfimaopnlem  25845  ellimc3  26069  eldv  26088  eltayl  26554  atandm3  27074  noetasuplem4  27931  dfprlng2  29228  rmoxfrd  32886  opeldifid  32991  2ndpreima  33100  f1od2  33110  ordtconnlem1  34354  bnj1253  35446  usgrgt2cycl  35643  satfdm  35874  wl-dral1d  38219  wl-sb8eft  38239  wl-sb8et  38241  wl-equsb3  38244  wl-sb8eut  38266  wl-sb8eutv  38267  wl-issetft  38270  poimirlem2  38306  poimirlem16  38320  poimirlem18  38322  poimirlem21  38325  poimirlem22  38326  eqbrrdv2  39670  islpln5  40342  islvol5  40386  ntrneicls11  44849  radcnvrat  45057  trsbc  45282  iindif2f  45911  ichnreuop  48254  ichreuopeq  48255  pm5.32dav  49605  exp12bd  49607  reuxfr1dd  49618  aacllem  50654