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  2038  cbvexdw  2340  cbvexd  2412  cbvrexdva  3223  raleq  3302  rexeqbidvvOLD  3316  cbvrexdva2  3328  rexeqf  3333  cbvexeqsetf  3474  dfsbcq2  3768  unineq  4263  iindif2  5053  reusv2  5373  rabxfrd  5387  opeqex  5473  eqbrrdv  5772  eqbrrdiv  5773  opelco2g  5847  opelcnvg  5860  ralrnmptw  7083  ralrnmpt  7085  fliftcnv  7303  eusvobj2  7395  br1steqg  8008  br2ndeqg  8009  ottpos  8233  smoiso  8374  ercnv  8738  ordiso2  9527  cantnfrescl  9688  cantnfp1lem3  9692  cantnflem1b  9698  cantnflem1  9701  cnfcom  9712  cnfcom3lem  9715  djulf1o  9924  djurf1o  9925  carden2  9999  cardeq0  10564  axpownd  10613  fpwwe2lem8  10650  fzen  13556  hasheq0  14379  incexc2  15852  divalglem4  16413  divalglem8  16417  divalgb  16421  sadadd  16484  sadass  16488  smuval2  16499  smumul  16510  isprm3  16700  vdwmc  16996  imasleval  17553  acsfn2  17673  invsym2  17774  yoniso  18295  pmtrfmvdn0  19441  dprd2d2  20025  cmpfi  23344  xkoinjcn  23623  tgpconncomp  24049  iscau3  25228  mbfimaopnlem  25606  ellimc3  25830  eldv  25849  eltayl  26317  atandm3  26838  noetasuplem4  27698  rmoxfrd  32420  opeldifid  32526  2ndpreima  32631  f1od2  32644  ordtconnlem1  33901  bnj1253  34994  usgrgt2cycl  35098  satfdm  35337  wl-dral1d  37495  wl-sb8eft  37515  wl-sb8et  37517  wl-equsb3  37520  wl-sb8eut  37542  wl-sb8eutv  37543  wl-issetft  37546  wl-ax11-lem8  37556  poimirlem2  37592  poimirlem16  37606  poimirlem18  37608  poimirlem21  37611  poimirlem22  37612  eqbrrdv2  38827  islpln5  39500  islvol5  39544  ntrneicls11  44061  radcnvrat  44286  trsbc  44513  iindif2f  45132  ichnreuop  47434  ichreuopeq  47435  pm5.32dav  48721  exp12bd  48723  reuxfr1dd  48733  aacllem  49613