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 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  318  cador  1610  cbvexdvaw  2043  cbvexdw  2336  cbvexd  2408  cbvrexdva  3238  raleq  3323  rexeqbidvvOLD  3333  cbvrexdva2  3346  rexeqf  3351  vtoclgft  3541  dfsbcq2  3780  unineq  4277  iindif2  5080  reusv2  5401  rabxfrd  5415  opeqex  5498  eqbrrdv  5792  eqbrrdiv  5793  opelco2g  5866  opelcnvg  5879  ralrnmptw  7093  ralrnmpt  7095  fliftcnv  7305  eusvobj2  7398  br1steqg  7994  br2ndeqg  7995  ottpos  8218  smoiso  8359  ercnv  8721  ordiso2  9507  cantnfrescl  9668  cantnfp1lem3  9672  cantnflem1b  9678  cantnflem1  9681  cnfcom  9692  cnfcom3lem  9695  djulf1o  9904  djurf1o  9905  carden2  9979  cardeq0  10544  axpownd  10593  fpwwe2lem8  10630  fzen  13515  hasheq0  14320  incexc2  15781  divalglem4  16336  divalglem8  16340  divalgb  16344  sadadd  16405  sadass  16409  smuval2  16420  smumul  16431  isprm3  16617  vdwmc  16908  imasleval  17484  acsfn2  17604  invsym2  17707  yoniso  18235  pmtrfmvdn0  19325  dprd2d2  19909  cmpfi  22904  xkoinjcn  23183  tgpconncomp  23609  iscau3  24787  mbfimaopnlem  25164  ellimc3  25388  eldv  25407  eltayl  25864  atandm3  26373  noetasuplem4  27229  rmoxfrd  31721  opeldifid  31818  2ndpreima  31917  f1od2  31934  ordtconnlem1  32893  bnj1253  34017  usgrgt2cycl  34110  satfdm  34349  wl-dral1d  36389  wl-sb8et  36407  wl-equsb3  36410  wl-sb8eut  36431  wl-issetft  36433  wl-ax11-lem8  36443  poimirlem2  36479  poimirlem16  36493  poimirlem18  36495  poimirlem21  36498  poimirlem22  36499  eqbrrdv2  37722  islpln5  38395  islvol5  38439  ntrneicls11  42827  radcnvrat  43059  trsbc  43287  iindif2f  43840  ichnreuop  46127  ichreuopeq  46128  pm5.32dav  47433  exp12bd  47435  aacllem  47802