Theorem 3bitr3g 313

Description: More general version of 3bitr3i 301. 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 285	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	bitrdi 287	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  318  cador  1610  cbvexdvaw  2043  cbvexdw  2336  cbvexd  2408  cbvrexdva  3238  raleq  3323  rexeqbidvvOLD  3333  cbvrexdva2  3346  rexeqf  3351  vtoclgft  3541  dfsbcq2  3781  unineq  4278  iindif2  5081  reusv2  5402  rabxfrd  5416  opeqex  5499  eqbrrdv  5794  eqbrrdiv  5795  opelco2g  5868  opelcnvg  5881  ralrnmptw  7096  ralrnmpt  7098  fliftcnv  7308  eusvobj2  7401  br1steqg  7997  br2ndeqg  7998  ottpos  8221  smoiso  8362  ercnv  8724  ordiso2  9510  cantnfrescl  9671  cantnfp1lem3  9675  cantnflem1b  9681  cantnflem1  9684  cnfcom  9695  cnfcom3lem  9698  djulf1o  9907  djurf1o  9908  carden2  9982  cardeq0  10547  axpownd  10596  fpwwe2lem8  10633  fzen  13518  hasheq0  14323  incexc2  15784  divalglem4  16339  divalglem8  16343  divalgb  16347  sadadd  16408  sadass  16412  smuval2  16423  smumul  16434  isprm3  16620  vdwmc  16911  imasleval  17487  acsfn2  17607  invsym2  17710  yoniso  18238  pmtrfmvdn0  19330  dprd2d2  19914  cmpfi  22912  xkoinjcn  23191  tgpconncomp  23617  iscau3  24795  mbfimaopnlem  25172  ellimc3  25396  eldv  25415  eltayl  25872  atandm3  26383  noetasuplem4  27239  rmoxfrd  31733  opeldifid  31830  2ndpreima  31929  f1od2  31946  ordtconnlem1  32904  bnj1253  34028  usgrgt2cycl  34121  satfdm  34360  wl-dral1d  36400  wl-sb8et  36418  wl-equsb3  36421  wl-sb8eut  36442  wl-issetft  36444  wl-ax11-lem8  36454  poimirlem2  36490  poimirlem16  36504  poimirlem18  36506  poimirlem21  36509  poimirlem22  36510  eqbrrdv2  37733  islpln5  38406  islvol5  38450  ntrneicls11  42841  radcnvrat  43073  trsbc  43301  iindif2f  43854  ichnreuop  46140  ichreuopeq  46141  pm5.32dav  47479  exp12bd  47481  aacllem  47848