Theorem 3bitr3g 305

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  notbid  310  cador  1666  cbvexd  2373  cbvexdva  2377  dfsbcq2  3655  unineq  4104  iindif2  4824  reusv2  5117  rabxfrd  5131  opeqex  5195  eqbrrdv  5466  eqbrrdiv  5467  opelco2g  5537  opelcnvg  5550  ralrnmpt  6634  fliftcnv  6835  eusvobj2  6917  br1steqg  7469  br2ndeqg  7470  ottpos  7646  smoiso  7744  ercnv  8049  ordiso2  8711  cantnfrescl  8872  cantnfp1lem3  8876  cantnflem1b  8882  cantnflem1  8885  cnfcom  8896  cnfcom3lem  8899  djulf1o  9073  djurf1o  9074  carden2  9148  cardeq0  9711  axpownd  9760  fpwwe2lem9  9797  fzen  12680  hasheq0  13475  incexc2  14983  divalglem4  15536  divalglem8  15540  divalgb  15544  sadadd  15605  sadass  15609  smuval2  15620  smumul  15631  isprm3  15812  vdwmc  16097  imasleval  16598  acsfn2  16720  invsym2  16819  yoniso  17322  pmtrfmvdn0  18276  dprd2d2  18841  cmpfi  21631  xkoinjcn  21910  tgpconncomp  22335  iscau3  23495  mbfimaopnlem  23870  ellimc3  24091  eldv  24110  eltayl  24562  atandm3  25067  rmoxfrd  29916  opeldifid  29992  2ndpreima  30068  f1od2  30082  ordtconnlem1  30576  bnj1253  31692  noetalem3  32462  wl-dral1d  33919  wl-sb8et  33936  wl-equsb3  33939  wl-sb8eut  33960  wl-ax11-lem8  33970  wl-clelsb3df  34005  poimirlem2  34046  poimirlem16  34060  poimirlem18  34062  poimirlem21  34065  poimirlem22  34066  eqbrrdv2  35026  islpln5  35698  islvol5  35742  ntrneicls11  39358  radcnvrat  39483  trsbc  39714  aacllem  43667