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  2406  cbvrexdva  3218  raleq  3296  rexeqbidvvOLD  3310  cbvrexdva2  3322  rexeqf  3330  cbvexeqsetf  3462  dfsbcq2  3756  unineq  4251  iindif2  5041  reusv2  5358  rabxfrd  5372  opeqex  5458  eqbrrdv  5756  eqbrrdiv  5757  opelco2g  5831  opelcnvg  5844  ralrnmptw  7066  ralrnmpt  7068  fliftcnv  7286  eusvobj2  7379  br1steqg  7990  br2ndeqg  7991  ottpos  8215  smoiso  8331  ercnv  8692  ordiso2  9468  cantnfrescl  9629  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1  9642  cnfcom  9653  cnfcom3lem  9656  djulf1o  9865  djurf1o  9866  carden2  9940  cardeq0  10505  axpownd  10554  fpwwe2lem8  10591  fzen  13502  hasheq0  14328  incexc2  15804  divalglem4  16366  divalglem8  16370  divalgb  16374  sadadd  16437  sadass  16441  smuval2  16452  smumul  16463  isprm3  16653  vdwmc  16949  imasleval  17504  acsfn2  17624  invsym2  17725  yoniso  18246  pmtrfmvdn0  19392  dprd2d2  19976  cmpfi  23295  xkoinjcn  23574  tgpconncomp  24000  iscau3  25178  mbfimaopnlem  25556  ellimc3  25780  eldv  25799  eltayl  26267  atandm3  26788  noetasuplem4  27648  rmoxfrd  32422  opeldifid  32528  2ndpreima  32631  f1od2  32644  ordtconnlem1  33914  bnj1253  35007  usgrgt2cycl  35117  satfdm  35356  wl-dral1d  37519  wl-sb8eft  37539  wl-sb8et  37541  wl-equsb3  37544  wl-sb8eut  37566  wl-sb8eutv  37567  wl-issetft  37570  wl-ax11-lem8  37580  poimirlem2  37616  poimirlem16  37630  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  eqbrrdv2  38856  islpln5  39529  islvol5  39573  ntrneicls11  44079  radcnvrat  44303  trsbc  44530  iindif2f  45154  ichnreuop  47473  ichreuopeq  47474  pm5.32dav  48782  exp12bd  48784  reuxfr1dd  48795  aacllem  49790