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  1611  cbvexdvaw  2043  cbvexdw  2338  cbvexd  2408  rexeqbidvv  3330  vtoclgft  3482  dfsbcq2  3714  unineq  4208  iindif2  5002  reusv2  5321  rabxfrd  5335  opeqex  5406  eqbrrdv  5692  eqbrrdiv  5693  opelco2g  5765  opelcnvg  5778  ralrnmptw  6952  ralrnmpt  6954  fliftcnv  7162  eusvobj2  7248  br1steqg  7826  br2ndeqg  7827  ottpos  8023  smoiso  8164  ercnv  8477  ordiso2  9204  cantnfrescl  9364  cantnfp1lem3  9368  cantnflem1b  9374  cantnflem1  9377  cnfcom  9388  cnfcom3lem  9391  djulf1o  9601  djurf1o  9602  carden2  9676  cardeq0  10239  axpownd  10288  fpwwe2lem8  10325  fzen  13202  hasheq0  14006  incexc2  15478  divalglem4  16033  divalglem8  16037  divalgb  16041  sadadd  16102  sadass  16106  smuval2  16117  smumul  16128  isprm3  16316  vdwmc  16607  imasleval  17169  acsfn2  17289  invsym2  17392  yoniso  17919  pmtrfmvdn0  18985  dprd2d2  19562  cmpfi  22467  xkoinjcn  22746  tgpconncomp  23172  iscau3  24347  mbfimaopnlem  24724  ellimc3  24948  eldv  24967  eltayl  25424  atandm3  25933  rmoxfrd  30742  opeldifid  30839  2ndpreima  30942  f1od2  30958  ordtconnlem1  31776  bnj1253  32897  usgrgt2cycl  32992  satfdm  33231  noetasuplem4  33866  wl-dral1d  35617  wl-sb8et  35635  wl-equsb3  35638  wl-sb8eut  35659  wl-ax11-lem8  35670  poimirlem2  35706  poimirlem16  35720  poimirlem18  35722  poimirlem21  35725  poimirlem22  35726  eqbrrdv2  36804  islpln5  37476  islvol5  37520  ntrneicls11  41589  radcnvrat  41821  trsbc  42049  ichnreuop  44812  ichreuopeq  44813  pm5.32dav  46027  exp12bd  46029  aacllem  46391