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  2039  cbvexdw  2337  cbvexd  2407  cbvrexdva  3219  raleq  3298  rexeqbidvvOLD  3312  cbvrexdva2  3324  rexeqf  3332  cbvexeqsetf  3465  dfsbcq2  3759  unineq  4254  iindif2  5044  reusv2  5361  rabxfrd  5375  opeqex  5461  eqbrrdv  5759  eqbrrdiv  5760  opelco2g  5834  opelcnvg  5847  ralrnmptw  7069  ralrnmpt  7071  fliftcnv  7289  eusvobj2  7382  br1steqg  7993  br2ndeqg  7994  ottpos  8218  smoiso  8334  ercnv  8695  ordiso2  9475  cantnfrescl  9636  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1  9649  cnfcom  9660  cnfcom3lem  9663  djulf1o  9872  djurf1o  9873  carden2  9947  cardeq0  10512  axpownd  10561  fpwwe2lem8  10598  fzen  13509  hasheq0  14335  incexc2  15811  divalglem4  16373  divalglem8  16377  divalgb  16381  sadadd  16444  sadass  16448  smuval2  16459  smumul  16470  isprm3  16660  vdwmc  16956  imasleval  17511  acsfn2  17631  invsym2  17732  yoniso  18253  pmtrfmvdn0  19399  dprd2d2  19983  cmpfi  23302  xkoinjcn  23581  tgpconncomp  24007  iscau3  25185  mbfimaopnlem  25563  ellimc3  25787  eldv  25806  eltayl  26274  atandm3  26795  noetasuplem4  27655  rmoxfrd  32429  opeldifid  32535  2ndpreima  32638  f1od2  32651  ordtconnlem1  33921  bnj1253  35014  usgrgt2cycl  35124  satfdm  35363  wl-dral1d  37526  wl-sb8eft  37546  wl-sb8et  37548  wl-equsb3  37551  wl-sb8eut  37573  wl-sb8eutv  37574  wl-issetft  37577  wl-ax11-lem8  37587  poimirlem2  37623  poimirlem16  37637  poimirlem18  37639  poimirlem21  37642  poimirlem22  37643  eqbrrdv2  38863  islpln5  39536  islvol5  39580  ntrneicls11  44086  radcnvrat  44310  trsbc  44537  iindif2f  45161  ichnreuop  47477  ichreuopeq  47478  pm5.32dav  48786  exp12bd  48788  reuxfr1dd  48799  aacllem  49794