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  1640  cbvexdvaw  2071  cbvexdw  2368  cbvexd  2437  cbvrexdva  3243  raleq  3316  cbvrexdva2  3337  rexeqf  3342  cbvexeqsetf  3465  dfsbcq2  3741  unineq  4232  iindif2  5036  reusv2  5365  rabxfrd  5379  opeqex  5470  eqbrrdv  5770  eqbrrdiv  5771  opelco2g  5846  opelcnvg  5859  ralrnmptw  7099  ralrnmpt  7101  fliftcnv  7323  eusvobj2  7416  br1steqg  8027  br2ndeqg  8028  f1od2  8114  ottpos  8260  smoiso  8377  ercnv  8746  ordiso2  9516  cantnfrescl  9684  cantnfp1lem3  9688  cantnflem1b  9694  cantnflem1  9697  cnfcom  9708  cnfcom3lem  9711  djulf1o  10000  djurf1o  10001  carden2  10075  cardeq0  10643  axpownd  10693  fpwwe2lem8  10730  fzen  13681  hasheq0  14514  incexc2  16016  divalglem4  16575  divalglem8  16579  divalgb  16583  sadadd  16646  sadass  16650  smuval2  16661  smumul  16672  isprm3  16867  vdwmc  17165  imasleval  17722  acsfn2  17846  invsym2  17947  yoniso  18468  pmtrfmvdn0  19685  dprd2d2  20269  cmpfi  23735  xkoinjcn  24015  tgpconncomp  24441  iscau3  25608  mbfimaopnlem  25985  ellimc3  26208  eldv  26227  eltayl  26696  atandm3  27215  noetasuplem4  28102  dfprlng2  29434  rmoxfrd  33140  opeldifid  33244  2ndpreima  33352  ordtconnlem1  34606  bnj1253  35697  usgrgt2cycl  35989  satfdm  36224  wl-dral1d  38572  wl-sb8eft  38592  wl-sb8et  38594  wl-equsb3  38597  wl-sb8eut  38619  wl-sb8eutv  38620  wl-issetft  38623  poimirlem2  38649  poimirlem16  38663  poimirlem18  38665  poimirlem21  38668  poimirlem22  38669  eqbrrdv2  40029  islpln5  40701  islvol5  40745  ntrneicls11  45199  radcnvrat  45407  trsbc  45631  iindif2f  46283  ichnreuop  48662  ichreuopeq  48663  pm5.32rda  50012  exp12bd  50014  reuxfr1dd  50025  aacllem  51122