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  1605  cbvexdvaw  2038  cbvexdw  2345  cbvexd  2416  cbvrexdva  3246  raleq  3331  rexeqbidvvOLD  3345  cbvrexdva2  3357  rexeqf  3362  cbvexeqsetf  3503  dfsbcq2  3807  unineq  4307  iindif2  5100  reusv2  5421  rabxfrd  5435  opeqex  5517  eqbrrdv  5817  eqbrrdiv  5818  opelco2g  5892  opelcnvg  5905  ralrnmptw  7128  ralrnmpt  7130  fliftcnv  7347  eusvobj2  7440  br1steqg  8052  br2ndeqg  8053  ottpos  8277  smoiso  8418  ercnv  8784  ordiso2  9584  cantnfrescl  9745  cantnfp1lem3  9749  cantnflem1b  9755  cantnflem1  9758  cnfcom  9769  cnfcom3lem  9772  djulf1o  9981  djurf1o  9982  carden2  10056  cardeq0  10621  axpownd  10670  fpwwe2lem8  10707  fzen  13601  hasheq0  14412  incexc2  15886  divalglem4  16444  divalglem8  16448  divalgb  16452  sadadd  16513  sadass  16517  smuval2  16528  smumul  16539  isprm3  16730  vdwmc  17025  imasleval  17601  acsfn2  17721  invsym2  17824  yoniso  18355  pmtrfmvdn0  19504  dprd2d2  20088  cmpfi  23437  xkoinjcn  23716  tgpconncomp  24142  iscau3  25331  mbfimaopnlem  25709  ellimc3  25934  eldv  25953  eltayl  26419  atandm3  26939  noetasuplem4  27799  rmoxfrd  32521  opeldifid  32621  2ndpreima  32719  f1od2  32735  ordtconnlem1  33870  bnj1253  34993  usgrgt2cycl  35098  satfdm  35337  wl-dral1d  37485  wl-sb8eft  37505  wl-sb8et  37507  wl-equsb3  37510  wl-sb8eut  37532  wl-sb8eutv  37533  wl-issetft  37536  wl-ax11-lem8  37546  poimirlem2  37582  poimirlem16  37596  poimirlem18  37598  poimirlem21  37601  poimirlem22  37602  eqbrrdv2  38819  islpln5  39492  islvol5  39536  ntrneicls11  44052  radcnvrat  44283  trsbc  44511  iindif2f  45065  ichnreuop  47346  ichreuopeq  47347  pm5.32dav  48527  exp12bd  48529  aacllem  48895