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  1638  cbvexdvaw  2069  cbvexdw  2371  cbvexd  2440  cbvrexdva  3246  raleq  3320  cbvrexdva2  3341  rexeqf  3346  cbvexeqsetf  3470  dfsbcq2  3747  unineq  4241  iindif2  5043  reusv2  5374  rabxfrd  5388  opeqex  5481  eqbrrdv  5779  eqbrrdiv  5780  opelco2g  5853  opelcnvg  5866  ralrnmptw  7089  ralrnmpt  7091  fliftcnv  7309  eusvobj2  7402  br1steqg  8004  br2ndeqg  8005  ottpos  8228  smoiso  8345  ercnv  8712  ordiso2  9473  cantnfrescl  9641  cantnfp1lem3  9645  cantnflem1b  9651  cantnflem1  9654  cnfcom  9665  cnfcom3lem  9668  djulf1o  9894  djurf1o  9895  carden2  9969  cardeq0  10531  axpownd  10581  fpwwe2lem8  10618  fzen  13564  hasheq0  14395  incexc2  15888  divalglem4  16449  divalglem8  16453  divalgb  16457  sadadd  16520  sadass  16524  smuval2  16535  smumul  16546  isprm3  16736  vdwmc  17033  imasleval  17590  acsfn2  17714  invsym2  17815  yoniso  18336  pmtrfmvdn0  19527  dprd2d2  20111  cmpfi  23565  xkoinjcn  23844  tgpconncomp  24270  iscau3  25437  mbfimaopnlem  25814  ellimc3  26038  eldv  26057  eltayl  26523  atandm3  27043  noetasuplem4  27900  dfprlng2  29197  rmoxfrd  32839  opeldifid  32944  2ndpreima  33053  f1od2  33064  ordtconnlem1  34314  bnj1253  35405  usgrgt2cycl  35622  satfdm  35861  wl-dral1d  38186  wl-sb8eft  38206  wl-sb8et  38208  wl-equsb3  38211  wl-sb8eut  38233  wl-sb8eutv  38234  wl-issetft  38237  poimirlem2  38273  poimirlem16  38287  poimirlem18  38289  poimirlem21  38292  poimirlem22  38293  eqbrrdv2  39637  islpln5  40309  islvol5  40353  ntrneicls11  44816  radcnvrat  45024  trsbc  45249  iindif2f  45878  ichnreuop  48221  ichreuopeq  48222  pm5.32dav  49572  exp12bd  49574  reuxfr1dd  49585  aacllem  50621