Theorem 3bitr3g 301

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  notbid  307  cador  1538  equequ2OLD  1942  cbvexdva  2271  dfsbcq2  3405  unineq  3836  iindif2  4525  reusv2  4800  rabxfrd  4815  opeqex  4887  eqbrrdv  5140  eqbrrdiv  5141  opelco2g  5211  opelcnvg  5224  ralrnmpt  6276  fliftcnv  6461  eusvobj2  6542  ottpos  7249  smoiso  7346  ercnv  7650  ordiso2  8303  cantnfrescl  8456  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1  8469  cnfcom  8480  cnfcom3lem  8483  carden2  8696  cardeq0  9253  axpownd  9302  fpwwe2lem9  9339  fzen  12229  hasheq0  13015  incexc2  14409  divalglem4  14957  divalglem8  14961  divalgb  14965  divalgmodOLD  14968  sadadd  15027  sadass  15031  smuval2  15042  smumul  15053  isprm3  15234  vdwmc  15520  imasleval  16024  acsfn2  16147  invsym2  16246  yoniso  16748  pmtrfmvdn0  17705  dprd2d2  18266  cmpfi  21021  xkoinjcn  21300  tgpconcomp  21726  iscau3  22884  mbfimaopnlem  23228  ellimc3  23449  eldv  23468  eltayl  23918  atandm3  24405  el2wlkonot  26396  el2spthonot  26397  rmoxfrdOLD  28716  rmoxfrd  28717  opeldifid  28794  2ndpreima  28868  f1od2  28887  ordtconlem1  29298  bnj1253  30339  wl-dral1d  32497  wl-sb8et  32513  wl-equsb3  32516  wl-sb8eut  32538  wl-ax11-lem8  32548  poimirlem2  32581  poimirlem16  32595  poimirlem18  32597  poimirlem21  32600  poimirlem22  32601  eqbrrdv2  33166  islpln5  33839  islvol5  33883  ntrneicls11  37408  radcnvrat  37535  trsbc  37771  aacllem  42356