Theorem 3bitr3g 316

Description: More general version of 3bitr3i 304. 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 288	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	bitrdi 290	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  notbid  321  cador  1635  cbvexdvaw  2066  cbvexdw  2377  cbvexd  2446  cbvrexdva  3252  raleq  3326  cbvrexdva2  3348  rexeqf  3353  cbvexeqsetf  3478  dfsbcq2  3756  unineq  4249  iindif2  5047  reusv2  5375  rabxfrd  5389  opeqex  5482  eqbrrdv  5780  eqbrrdiv  5781  opelco2g  5854  opelcnvg  5867  ralrnmptw  7090  ralrnmpt  7092  fliftcnv  7310  eusvobj2  7403  br1steqg  8008  br2ndeqg  8009  ottpos  8232  smoiso  8349  ercnv  8716  ordiso2  9477  cantnfrescl  9645  cantnfp1lem3  9649  cantnflem1b  9655  cantnflem1  9658  cnfcom  9669  cnfcom3lem  9672  djulf1o  9898  djurf1o  9899  carden2  9973  cardeq0  10536  axpownd  10586  fpwwe2lem8  10623  fzen  13569  hasheq0  14399  incexc2  15892  divalglem4  16454  divalglem8  16458  divalgb  16462  sadadd  16525  sadass  16529  smuval2  16540  smumul  16551  isprm3  16741  vdwmc  17038  imasleval  17595  acsfn2  17719  invsym2  17820  yoniso  18341  pmtrfmvdn0  19532  dprd2d2  20116  cmpfi  23534  xkoinjcn  23813  tgpconncomp  24239  iscau3  25406  mbfimaopnlem  25783  ellimc3  26007  eldv  26026  eltayl  26489  atandm3  27009  noetasuplem4  27866  rmoxfrd  32780  opeldifid  32885  2ndpreima  32994  f1od2  33005  ordtconnlem1  34259  bnj1253  35350  usgrgt2cycl  35521  satfdm  35760  wl-dral1d  38074  wl-sb8eft  38094  wl-sb8et  38096  wl-equsb3  38099  wl-sb8eut  38121  wl-sb8eutv  38122  wl-issetft  38125  poimirlem2  38161  poimirlem16  38175  poimirlem18  38177  poimirlem21  38180  poimirlem22  38181  eqbrrdv2  39527  islpln5  40199  islvol5  40243  ntrneicls11  44708  radcnvrat  44916  trsbc  45141  iindif2f  45770  ichnreuop  48110  ichreuopeq  48111  pm5.32dav  49457  exp12bd  49459  reuxfr1dd  49470  aacllem  50475