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  1610  cbvexdvaw  2041  cbvexdw  2344  cbvexd  2413  cbvrexdva  3219  raleq  3293  cbvrexdva2  3315  rexeqf  3320  cbvexeqsetf  3445  dfsbcq2  3732  unineq  4229  iindif2  5020  reusv2  5340  rabxfrd  5354  opeqex  5446  eqbrrdv  5742  eqbrrdiv  5743  opelco2g  5816  opelcnvg  5829  ralrnmptw  7040  ralrnmpt  7042  fliftcnv  7259  eusvobj2  7352  br1steqg  7957  br2ndeqg  7958  ottpos  8179  smoiso  8295  ercnv  8658  ordiso2  9423  cantnfrescl  9588  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1  9601  cnfcom  9612  cnfcom3lem  9615  djulf1o  9827  djurf1o  9828  carden2  9902  cardeq0  10465  axpownd  10515  fpwwe2lem8  10552  fzen  13486  hasheq0  14316  incexc2  15794  divalglem4  16356  divalglem8  16360  divalgb  16364  sadadd  16427  sadass  16431  smuval2  16442  smumul  16453  isprm3  16643  vdwmc  16940  imasleval  17496  acsfn2  17620  invsym2  17721  yoniso  18242  pmtrfmvdn0  19428  dprd2d2  20012  cmpfi  23383  xkoinjcn  23662  tgpconncomp  24088  iscau3  25255  mbfimaopnlem  25632  ellimc3  25856  eldv  25875  eltayl  26336  atandm3  26855  noetasuplem4  27714  rmoxfrd  32577  opeldifid  32684  2ndpreima  32796  f1od2  32807  ordtconnlem1  34084  bnj1253  35175  usgrgt2cycl  35328  satfdm  35567  wl-dral1d  37870  wl-sb8eft  37890  wl-sb8et  37892  wl-equsb3  37895  wl-sb8eut  37917  wl-sb8eutv  37918  wl-issetft  37921  poimirlem2  37957  poimirlem16  37971  poimirlem18  37973  poimirlem21  37976  poimirlem22  37977  eqbrrdv2  39323  islpln5  39995  islvol5  40039  ntrneicls11  44535  radcnvrat  44759  trsbc  44985  iindif2f  45608  ichnreuop  47944  ichreuopeq  47945  pm5.32dav  49281  exp12bd  49283  reuxfr1dd  49294  aacllem  50288