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 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  notbid  321  cador  1635  cbvexdvaw  2066  cbvexdw  2377  cbvexd  2446  cbvrexdva  3252  raleq  3326  cbvrexdva2  3348  rexeqf  3353  cbvexeqsetf  3478  dfsbcq2  3756  unineq  4249  iindif2  5044  reusv2  5372  rabxfrd  5386  opeqex  5479  eqbrrdv  5777  eqbrrdiv  5778  opelco2g  5851  opelcnvg  5864  ralrnmptw  7087  ralrnmpt  7089  fliftcnv  7307  eusvobj2  7400  br1steqg  8004  br2ndeqg  8005  ottpos  8228  smoiso  8345  ercnv  8712  ordiso2  9473  cantnfrescl  9641  cantnfp1lem3  9645  cantnflem1b  9651  cantnflem1  9654  cnfcom  9665  cnfcom3lem  9668  djulf1o  9894  djurf1o  9895  carden2  9969  cardeq0  10532  axpownd  10582  fpwwe2lem8  10619  fzen  13565  hasheq0  14395  incexc2  15888  divalglem4  16450  divalglem8  16454  divalgb  16458  sadadd  16521  sadass  16525  smuval2  16536  smumul  16547  isprm3  16737  vdwmc  17034  imasleval  17591  acsfn2  17715  invsym2  17816  yoniso  18337  pmtrfmvdn0  19528  dprd2d2  20112  cmpfi  23530  xkoinjcn  23809  tgpconncomp  24235  iscau3  25402  mbfimaopnlem  25779  ellimc3  26003  eldv  26022  eltayl  26485  atandm3  27005  noetasuplem4  27862  rmoxfrd  32776  opeldifid  32881  2ndpreima  32990  f1od2  33001  ordtconnlem1  34255  bnj1253  35346  usgrgt2cycl  35517  satfdm  35756  wl-dral1d  38069  wl-sb8eft  38089  wl-sb8et  38091  wl-equsb3  38094  wl-sb8eut  38116  wl-sb8eutv  38117  wl-issetft  38120  poimirlem2  38156  poimirlem16  38170  poimirlem18  38172  poimirlem21  38175  poimirlem22  38176  eqbrrdv2  39522  islpln5  40194  islvol5  40238  ntrneicls11  44703  radcnvrat  44911  trsbc  45136  iindif2f  45765  ichnreuop  48105  ichreuopeq  48106  pm5.32dav  49452  exp12bd  49454  reuxfr1dd  49465  aacllem  50470