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  3286  rexeqbidvvOLD  3300  cbvrexdva2  3312  rexeqf  3319  cbvexeqsetf  3451  dfsbcq2  3745  unineq  4239  iindif2  5026  reusv2  5342  rabxfrd  5356  opeqex  5441  eqbrrdv  5736  eqbrrdiv  5737  opelco2g  5810  opelcnvg  5823  ralrnmptw  7028  ralrnmpt  7030  fliftcnv  7248  eusvobj2  7341  br1steqg  7946  br2ndeqg  7947  ottpos  8169  smoiso  8285  ercnv  8646  ordiso2  9407  cantnfrescl  9572  cantnfp1lem3  9576  cantnflem1b  9582  cantnflem1  9585  cnfcom  9596  cnfcom3lem  9599  djulf1o  9808  djurf1o  9809  carden2  9883  cardeq0  10446  axpownd  10495  fpwwe2lem8  10532  fzen  13444  hasheq0  14270  incexc2  15745  divalglem4  16307  divalglem8  16311  divalgb  16315  sadadd  16378  sadass  16382  smuval2  16393  smumul  16404  isprm3  16594  vdwmc  16890  imasleval  17445  acsfn2  17569  invsym2  17670  yoniso  18191  pmtrfmvdn0  19341  dprd2d2  19925  cmpfi  23293  xkoinjcn  23572  tgpconncomp  23998  iscau3  25176  mbfimaopnlem  25554  ellimc3  25778  eldv  25797  eltayl  26265  atandm3  26786  noetasuplem4  27646  rmoxfrd  32437  opeldifid  32543  2ndpreima  32650  f1od2  32663  ordtconnlem1  33891  bnj1253  34984  usgrgt2cycl  35103  satfdm  35342  wl-dral1d  37505  wl-sb8eft  37525  wl-sb8et  37527  wl-equsb3  37530  wl-sb8eut  37552  wl-sb8eutv  37553  wl-issetft  37556  wl-ax11-lem8  37566  poimirlem2  37602  poimirlem16  37616  poimirlem18  37618  poimirlem21  37621  poimirlem22  37622  eqbrrdv2  38842  islpln5  39514  islvol5  39558  ntrneicls11  44063  radcnvrat  44287  trsbc  44514  iindif2f  45138  ichnreuop  47456  ichreuopeq  47457  pm5.32dav  48778  exp12bd  48780  reuxfr1dd  48791  aacllem  49786