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  1607  cbvexdvaw  2040  cbvexdw  2333  cbvexd  2405  cbvrexdva  3235  raleq  3320  rexeqbidvvOLD  3330  cbvrexdva2  3343  rexeqf  3348  issetft  3486  dfsbcq2  3779  unineq  4276  iindif2  5079  reusv2  5400  rabxfrd  5414  opeqex  5497  eqbrrdv  5792  eqbrrdiv  5793  opelco2g  5866  opelcnvg  5879  ralrnmptw  7094  ralrnmpt  7096  fliftcnv  7310  eusvobj2  7403  br1steqg  7999  br2ndeqg  8000  ottpos  8223  smoiso  8364  ercnv  8726  ordiso2  9512  cantnfrescl  9673  cantnfp1lem3  9677  cantnflem1b  9683  cantnflem1  9686  cnfcom  9697  cnfcom3lem  9700  djulf1o  9909  djurf1o  9910  carden2  9984  cardeq0  10549  axpownd  10598  fpwwe2lem8  10635  fzen  13522  hasheq0  14327  incexc2  15788  divalglem4  16343  divalglem8  16347  divalgb  16351  sadadd  16412  sadass  16416  smuval2  16427  smumul  16438  isprm3  16624  vdwmc  16915  imasleval  17491  acsfn2  17611  invsym2  17714  yoniso  18242  pmtrfmvdn0  19371  dprd2d2  19955  cmpfi  23132  xkoinjcn  23411  tgpconncomp  23837  iscau3  25026  mbfimaopnlem  25404  ellimc3  25628  eldv  25647  eltayl  26108  atandm3  26619  noetasuplem4  27475  rmoxfrd  32000  opeldifid  32097  2ndpreima  32196  f1od2  32213  ordtconnlem1  33202  bnj1253  34326  usgrgt2cycl  34419  satfdm  34658  wl-dral1d  36703  wl-sb8et  36721  wl-equsb3  36724  wl-sb8eut  36745  wl-issetft  36747  wl-ax11-lem8  36757  poimirlem2  36793  poimirlem16  36807  poimirlem18  36809  poimirlem21  36812  poimirlem22  36813  eqbrrdv2  38036  islpln5  38709  islvol5  38753  ntrneicls11  43143  radcnvrat  43375  trsbc  43603  iindif2f  44155  ichnreuop  46438  ichreuopeq  46439  pm5.32dav  47566  exp12bd  47568  aacllem  47935