Theorem 3bitr3g 302

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  notbid  308  cador  1544  equequ2OLD  1957  cbvexdva  2287  dfsbcq2  3425  unineq  3858  iindif2  4560  reusv2  4839  rabxfrd  4854  opeqex  4927  eqbrrdv  5183  eqbrrdiv  5184  opelco2g  5254  opelcnvg  5267  ralrnmpt  6325  fliftcnv  6516  eusvobj2  6598  ottpos  7308  smoiso  7405  ercnv  7709  ordiso2  8365  cantnfrescl  8518  cantnfp1lem3  8522  cantnflem1b  8528  cantnflem1  8531  cnfcom  8542  cnfcom3lem  8545  carden2  8758  cardeq0  9319  axpownd  9368  fpwwe2lem9  9405  fzen  12297  hasheq0  13091  incexc2  14490  divalglem4  15038  divalglem8  15042  divalgb  15046  divalgmodOLD  15049  sadadd  15108  sadass  15112  smuval2  15123  smumul  15134  isprm3  15315  vdwmc  15601  imasleval  16117  acsfn2  16240  invsym2  16339  yoniso  16841  pmtrfmvdn0  17798  dprd2d2  18359  cmpfi  21116  xkoinjcn  21395  tgpconncomp  21821  iscau3  22979  mbfimaopnlem  23323  ellimc3  23544  eldv  23563  eltayl  24013  atandm3  24500  rmoxfrdOLD  29172  rmoxfrd  29173  opeldifid  29248  2ndpreima  29319  f1od2  29333  ordtconnlem1  29744  bnj1253  30785  wl-dral1d  32926  wl-sb8et  32942  wl-equsb3  32945  wl-sb8eut  32967  wl-ax11-lem8  32977  poimirlem2  33010  poimirlem16  33024  poimirlem18  33026  poimirlem21  33029  poimirlem22  33030  eqbrrdv2  33595  islpln5  34268  islvol5  34312  ntrneicls11  37837  radcnvrat  37962  trsbc  38199  aacllem  41805