Theorem 3bitr3g 312

Description: More general version of 3bitr3i 300. 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	bitr3id 284	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	bitrdi 286	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  notbid  317  cador  1602  cbvexdvaw  2035  cbvexdw  2330  cbvexd  2402  cbvrexdva  3228  raleq  3312  rexeqbidvvOLD  3322  cbvrexdva2  3333  rexeqf  3338  issetft  3477  dfsbcq2  3779  unineq  4279  iindif2  5085  reusv2  5407  rabxfrd  5421  opeqex  5504  eqbrrdv  5799  eqbrrdiv  5800  opelco2g  5874  opelcnvg  5887  ralrnmptw  7108  ralrnmpt  7110  fliftcnv  7323  eusvobj2  7416  br1steqg  8025  br2ndeqg  8026  ottpos  8251  smoiso  8392  ercnv  8755  ordiso2  9558  cantnfrescl  9719  cantnfp1lem3  9723  cantnflem1b  9729  cantnflem1  9732  cnfcom  9743  cnfcom3lem  9746  djulf1o  9955  djurf1o  9956  carden2  10030  cardeq0  10595  axpownd  10644  fpwwe2lem8  10681  fzen  13572  hasheq0  14380  incexc2  15842  divalglem4  16398  divalglem8  16402  divalgb  16406  sadadd  16467  sadass  16471  smuval2  16482  smumul  16493  isprm3  16684  vdwmc  16980  imasleval  17556  acsfn2  17676  invsym2  17779  yoniso  18310  pmtrfmvdn0  19460  dprd2d2  20044  cmpfi  23403  xkoinjcn  23682  tgpconncomp  24108  iscau3  25297  mbfimaopnlem  25675  ellimc3  25899  eldv  25918  eltayl  26387  atandm3  26906  noetasuplem4  27766  rmoxfrd  32421  opeldifid  32519  2ndpreima  32619  f1od2  32635  ordtconnlem1  33739  bnj1253  34862  usgrgt2cycl  34958  satfdm  35197  wl-dral1d  37226  wl-sb8eft  37246  wl-sb8et  37248  wl-equsb3  37251  wl-sb8eut  37273  wl-sb8eutv  37274  wl-issetft  37277  wl-ax11-lem8  37287  poimirlem2  37323  poimirlem16  37337  poimirlem18  37339  poimirlem21  37342  poimirlem22  37343  eqbrrdv2  38561  islpln5  39234  islvol5  39278  ntrneicls11  43757  radcnvrat  43988  trsbc  44216  iindif2f  44765  ichnreuop  47044  ichreuopeq  47045  pm5.32dav  48181  exp12bd  48183  aacllem  48549