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  2337  cbvexd  2409  rexeqbidvv  3340  vtoclgft  3493  dfsbcq2  3720  unineq  4212  iindif2  5007  reusv2  5327  rabxfrd  5341  opeqex  5413  eqbrrdv  5705  eqbrrdiv  5706  opelco2g  5779  opelcnvg  5792  ralrnmptw  6979  ralrnmpt  6981  fliftcnv  7191  eusvobj2  7277  br1steqg  7862  br2ndeqg  7863  ottpos  8061  smoiso  8202  ercnv  8528  ordiso2  9283  cantnfrescl  9443  cantnfp1lem3  9447  cantnflem1b  9453  cantnflem1  9456  cnfcom  9467  cnfcom3lem  9470  djulf1o  9679  djurf1o  9680  carden2  9754  cardeq0  10317  axpownd  10366  fpwwe2lem8  10403  fzen  13282  hasheq0  14087  incexc2  15559  divalglem4  16114  divalglem8  16118  divalgb  16122  sadadd  16183  sadass  16187  smuval2  16198  smumul  16209  isprm3  16397  vdwmc  16688  imasleval  17261  acsfn2  17381  invsym2  17484  yoniso  18012  pmtrfmvdn0  19079  dprd2d2  19656  cmpfi  22568  xkoinjcn  22847  tgpconncomp  23273  iscau3  24451  mbfimaopnlem  24828  ellimc3  25052  eldv  25071  eltayl  25528  atandm3  26037  rmoxfrd  30850  opeldifid  30947  2ndpreima  31049  f1od2  31065  ordtconnlem1  31883  bnj1253  33006  usgrgt2cycl  33101  satfdm  33340  noetasuplem4  33948  wl-dral1d  35699  wl-sb8et  35717  wl-equsb3  35720  wl-sb8eut  35741  wl-ax11-lem8  35752  poimirlem2  35788  poimirlem16  35802  poimirlem18  35804  poimirlem21  35807  poimirlem22  35808  eqbrrdv2  36884  islpln5  37556  islvol5  37600  ntrneicls11  41707  radcnvrat  41939  trsbc  42167  ichnreuop  44935  ichreuopeq  44936  pm5.32dav  46150  exp12bd  46152  aacllem  46516