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  1608  cbvexdvaw  2039  cbvexdw  2337  cbvexd  2406  cbvrexdva  3210  raleq  3287  rexeqbidvvOLD  3301  cbvrexdva2  3313  rexeqf  3321  cbvexeqsetf  3453  dfsbcq2  3747  unineq  4241  iindif2  5029  reusv2  5345  rabxfrd  5359  opeqex  5445  eqbrrdv  5740  eqbrrdiv  5741  opelco2g  5814  opelcnvg  5827  ralrnmptw  7032  ralrnmpt  7034  fliftcnv  7252  eusvobj2  7345  br1steqg  7953  br2ndeqg  7954  ottpos  8176  smoiso  8292  ercnv  8653  ordiso2  9426  cantnfrescl  9591  cantnfp1lem3  9595  cantnflem1b  9601  cantnflem1  9604  cnfcom  9615  cnfcom3lem  9618  djulf1o  9827  djurf1o  9828  carden2  9902  cardeq0  10465  axpownd  10514  fpwwe2lem8  10551  fzen  13463  hasheq0  14289  incexc2  15764  divalglem4  16326  divalglem8  16330  divalgb  16334  sadadd  16397  sadass  16401  smuval2  16412  smumul  16423  isprm3  16613  vdwmc  16909  imasleval  17464  acsfn2  17588  invsym2  17689  yoniso  18210  pmtrfmvdn0  19360  dprd2d2  19944  cmpfi  23312  xkoinjcn  23591  tgpconncomp  24017  iscau3  25195  mbfimaopnlem  25573  ellimc3  25797  eldv  25816  eltayl  26284  atandm3  26805  noetasuplem4  27665  rmoxfrd  32456  opeldifid  32562  2ndpreima  32669  f1od2  32682  ordtconnlem1  33910  bnj1253  35003  usgrgt2cycl  35122  satfdm  35361  wl-dral1d  37524  wl-sb8eft  37544  wl-sb8et  37546  wl-equsb3  37549  wl-sb8eut  37571  wl-sb8eutv  37572  wl-issetft  37575  wl-ax11-lem8  37585  poimirlem2  37621  poimirlem16  37635  poimirlem18  37637  poimirlem21  37640  poimirlem22  37641  eqbrrdv2  38861  islpln5  39534  islvol5  39578  ntrneicls11  44083  radcnvrat  44307  trsbc  44534  iindif2f  45158  ichnreuop  47476  ichreuopeq  47477  pm5.32dav  48798  exp12bd  48800  reuxfr1dd  48811  aacllem  49806