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 206

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 207

This theorem is referenced by:  notbid  318  cador  1609  cbvexdvaw  2040  cbvexdw  2339  cbvexd  2408  cbvrexdva  3213  raleq  3289  rexeqbidvvOLD  3303  cbvrexdva2  3315  rexeqf  3322  cbvexeqsetf  3451  dfsbcq2  3739  unineq  4233  iindif2  5020  reusv2  5336  rabxfrd  5350  opeqex  5433  eqbrrdv  5728  eqbrrdiv  5729  opelco2g  5802  opelcnvg  5815  ralrnmptw  7022  ralrnmpt  7024  fliftcnv  7240  eusvobj2  7333  br1steqg  7938  br2ndeqg  7939  ottpos  8161  smoiso  8277  ercnv  8638  ordiso2  9396  cantnfrescl  9561  cantnfp1lem3  9565  cantnflem1b  9571  cantnflem1  9574  cnfcom  9585  cnfcom3lem  9588  djulf1o  9800  djurf1o  9801  carden2  9875  cardeq0  10438  axpownd  10487  fpwwe2lem8  10524  fzen  13436  hasheq0  14265  incexc2  15740  divalglem4  16302  divalglem8  16306  divalgb  16310  sadadd  16373  sadass  16377  smuval2  16388  smumul  16399  isprm3  16589  vdwmc  16885  imasleval  17440  acsfn2  17564  invsym2  17665  yoniso  18186  pmtrfmvdn0  19369  dprd2d2  19953  cmpfi  23318  xkoinjcn  23597  tgpconncomp  24023  iscau3  25200  mbfimaopnlem  25578  ellimc3  25802  eldv  25821  eltayl  26289  atandm3  26810  noetasuplem4  27670  rmoxfrd  32464  opeldifid  32571  2ndpreima  32681  f1od2  32694  ordtconnlem1  33929  bnj1253  35021  usgrgt2cycl  35166  satfdm  35405  wl-dral1d  37565  wl-sb8eft  37585  wl-sb8et  37587  wl-equsb3  37590  wl-sb8eut  37612  wl-sb8eutv  37613  wl-issetft  37616  wl-ax11-lem8  37626  poimirlem2  37662  poimirlem16  37676  poimirlem18  37678  poimirlem21  37681  poimirlem22  37682  eqbrrdv2  38902  islpln5  39574  islvol5  39618  ntrneicls11  44123  radcnvrat  44347  trsbc  44573  iindif2f  45197  ichnreuop  47503  ichreuopeq  47504  pm5.32dav  48825  exp12bd  48827  reuxfr1dd  48838  aacllem  49833