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  1605  cbvexdvaw  2042  cbvexdw  2355  cbvexd  2425  cbvrexdva2OLD  3458  vtoclgft  3553  dfsbcq2  3774  unineq  4253  iindif2  4991  reusv2  5295  rabxfrd  5309  opeqex  5380  eqbrrdv  5660  eqbrrdiv  5661  opelco2g  5732  opelcnvg  5745  ralrnmptw  6854  ralrnmpt  6856  fliftcnv  7058  eusvobj2  7143  br1steqg  7705  br2ndeqg  7706  ottpos  7896  smoiso  7993  ercnv  8304  ordiso2  8973  cantnfrescl  9133  cantnfp1lem3  9137  cantnflem1b  9143  cantnflem1  9146  cnfcom  9157  cnfcom3lem  9160  djulf1o  9335  djurf1o  9336  carden2  9410  cardeq0  9968  axpownd  10017  fpwwe2lem9  10054  fzen  12918  hasheq0  13718  incexc2  15187  divalglem4  15741  divalglem8  15745  divalgb  15749  sadadd  15810  sadass  15814  smuval2  15825  smumul  15836  isprm3  16021  vdwmc  16308  imasleval  16808  acsfn2  16928  invsym2  17027  yoniso  17529  pmtrfmvdn0  18584  dprd2d2  19160  cmpfi  22010  xkoinjcn  22289  tgpconncomp  22715  iscau3  23875  mbfimaopnlem  24250  ellimc3  24471  eldv  24490  eltayl  24942  atandm3  25450  rmoxfrd  30251  opeldifid  30343  2ndpreima  30437  f1od2  30451  ordtconnlem1  31162  bnj1253  32284  usgrgt2cycl  32372  satfdm  32611  noetalem3  33214  wl-dral1d  34765  wl-sb8et  34783  wl-equsb3  34786  wl-sb8eut  34807  wl-ax11-lem8  34818  wl-clelsb3df  34857  poimirlem2  34888  poimirlem16  34902  poimirlem18  34904  poimirlem21  34907  poimirlem22  34908  eqbrrdv2  35993  islpln5  36665  islvol5  36709  ntrneicls11  40433  radcnvrat  40639  trsbc  40867  dfich2bi  43609  ichnreuop  43628  ichreuopeq  43629  aacllem  44896