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 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  notbid  321  cador  1641  cbvexdvaw  2074  cbvexdw  2372  cbvexd  2440  cbvrexdva  3247  raleq  3320  cbvrexdva2  3341  rexeqf  3346  cbvexeqsetf  3469  dfsbcq2  3745  unineq  4236  iindif2  5042  reusv2  5372  rabxfrd  5386  opeqex  5477  eqbrrdv  5778  eqbrrdiv  5779  opelco2g  5856  opelcnvg  5870  ralrnmptw  7126  ralrnmpt  7128  fliftcnv  7350  eusvobj2  7443  br1steqg  8057  br2ndeqg  8058  f1od2  8145  ottpos  8291  smoiso  8408  ercnv  8777  ordiso2  9546  cantnfrescl  9714  cantnfp1lem3  9718  cantnflem1b  9724  cantnflem1  9727  cnfcom  9738  cnfcom3lem  9741  djulf1o  10030  djurf1o  10031  carden2  10107  cardeq0  10675  axpownd  10725  fpwwe2lem8  10762  fzen  13714  hasheq0  14548  incexc2  16051  divalglem4  16610  divalglem8  16614  divalgb  16618  sadadd  16681  sadass  16685  smuval2  16696  smumul  16707  isprm3  16902  vdwmc  17200  imasleval  17763  acsfn2  17887  invsym2  17988  yoniso  18509  pmtrfmvdn0  19727  dprd2d2  20311  cmpfi  23781  xkoinjcn  24061  tgpconncomp  24487  iscau3  25654  mbfimaopnlem  26031  ellimc3  26254  eldv  26273  eltayl  26744  atandm3  27263  noetasuplem4  28150  dfprlng2  29482  rmoxfrd  33188  opeldifid  33291  2ndpreima  33398  ordtconnlem1  34667  bnj1253  35758  usgrgt2cycl  36107  satfdm  36342  wl-dral1d  38731  wl-sb8eft  38751  wl-sb8et  38753  wl-equsb3  38756  wl-sb8eut  38778  wl-sb8eutv  38779  wl-issetft  38782  poimirlem2  38808  poimirlem16  38822  poimirlem18  38824  poimirlem21  38827  poimirlem22  38828  eqbrrdv2  40186  islpln5  40858  islvol5  40902  ntrneicls11  45351  radcnvrat  45559  trsbc  45783  iindif2f  46448  ichnreuop  48827  ichreuopeq  48828  pm5.32rda  50235  exp12bd  50237  reuxfr1dd  50248  aacllem  51367