Theorem 3bitr3g 315

Description: More general version of 3bitr3i 303. 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	syl5bbr 287	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	syl6bb 289	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  notbid  320  cador  1609  cbvexdvaw  2046  cbvexdw  2359  cbvexd  2429  cbvrexdva2OLD  3458  vtoclgft  3553  dfsbcq2  3775  unineq  4254  iindif2  4999  reusv2  5304  rabxfrd  5318  opeqex  5388  eqbrrdv  5666  eqbrrdiv  5667  opelco2g  5738  opelcnvg  5751  ralrnmptw  6860  ralrnmpt  6862  fliftcnv  7064  eusvobj2  7149  br1steqg  7711  br2ndeqg  7712  ottpos  7902  smoiso  7999  ercnv  8310  ordiso2  8979  cantnfrescl  9139  cantnfp1lem3  9143  cantnflem1b  9149  cantnflem1  9152  cnfcom  9163  cnfcom3lem  9166  djulf1o  9341  djurf1o  9342  carden2  9416  cardeq0  9974  axpownd  10023  fpwwe2lem9  10060  fzen  12925  hasheq0  13725  incexc2  15193  divalglem4  15747  divalglem8  15751  divalgb  15755  sadadd  15816  sadass  15820  smuval2  15831  smumul  15842  isprm3  16027  vdwmc  16314  imasleval  16814  acsfn2  16934  invsym2  17033  yoniso  17535  pmtrfmvdn0  18590  dprd2d2  19166  cmpfi  22016  xkoinjcn  22295  tgpconncomp  22721  iscau3  23881  mbfimaopnlem  24256  ellimc3  24477  eldv  24496  eltayl  24948  atandm3  25456  rmoxfrd  30257  opeldifid  30349  2ndpreima  30443  f1od2  30457  ordtconnlem1  31167  bnj1253  32289  usgrgt2cycl  32377  satfdm  32616  noetalem3  33219  wl-dral1d  34786  wl-sb8et  34804  wl-equsb3  34807  wl-sb8eut  34828  wl-ax11-lem8  34839  wl-clelsb3df  34878  poimirlem2  34909  poimirlem16  34923  poimirlem18  34925  poimirlem21  34928  poimirlem22  34929  eqbrrdv2  36014  islpln5  36686  islvol5  36730  ntrneicls11  40460  radcnvrat  40666  trsbc  40894  dfich2bi  43635  ichnreuop  43654  ichreuopeq  43655  aacllem  44922