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  1608  cbvexdvaw  2038  cbvexdw  2341  cbvexd  2413  cbvrexdva  3240  raleq  3323  rexeqbidvvOLD  3337  cbvrexdva2  3349  rexeqf  3354  cbvexeqsetf  3495  dfsbcq2  3791  unineq  4288  iindif2  5077  reusv2  5403  rabxfrd  5417  opeqex  5503  eqbrrdv  5803  eqbrrdiv  5804  opelco2g  5878  opelcnvg  5891  ralrnmptw  7114  ralrnmpt  7116  fliftcnv  7331  eusvobj2  7423  br1steqg  8036  br2ndeqg  8037  ottpos  8261  smoiso  8402  ercnv  8766  ordiso2  9555  cantnfrescl  9716  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1  9729  cnfcom  9740  cnfcom3lem  9743  djulf1o  9952  djurf1o  9953  carden2  10027  cardeq0  10592  axpownd  10641  fpwwe2lem8  10678  fzen  13581  hasheq0  14402  incexc2  15874  divalglem4  16433  divalglem8  16437  divalgb  16441  sadadd  16504  sadass  16508  smuval2  16519  smumul  16530  isprm3  16720  vdwmc  17016  imasleval  17586  acsfn2  17706  invsym2  17807  yoniso  18330  pmtrfmvdn0  19480  dprd2d2  20064  cmpfi  23416  xkoinjcn  23695  tgpconncomp  24121  iscau3  25312  mbfimaopnlem  25690  ellimc3  25914  eldv  25933  eltayl  26401  atandm3  26921  noetasuplem4  27781  rmoxfrd  32512  opeldifid  32612  2ndpreima  32717  f1od2  32732  ordtconnlem1  33923  bnj1253  35031  usgrgt2cycl  35135  satfdm  35374  wl-dral1d  37532  wl-sb8eft  37552  wl-sb8et  37554  wl-equsb3  37557  wl-sb8eut  37579  wl-sb8eutv  37580  wl-issetft  37583  wl-ax11-lem8  37593  poimirlem2  37629  poimirlem16  37643  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  eqbrrdv2  38864  islpln5  39537  islvol5  39581  ntrneicls11  44103  radcnvrat  44333  trsbc  44560  iindif2f  45165  ichnreuop  47459  ichreuopeq  47460  pm5.32dav  48714  exp12bd  48716  reuxfr1dd  48726  aacllem  49320