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  2039  cbvexdw  2337  cbvexd  2406  cbvrexdva  3216  raleq  3293  rexeqbidvvOLD  3307  cbvrexdva2  3319  rexeqf  3327  cbvexeqsetf  3459  dfsbcq2  3753  unineq  4247  iindif2  5036  reusv2  5353  rabxfrd  5367  opeqex  5453  eqbrrdv  5747  eqbrrdiv  5748  opelco2g  5821  opelcnvg  5834  ralrnmptw  7048  ralrnmpt  7050  fliftcnv  7268  eusvobj2  7361  br1steqg  7969  br2ndeqg  7970  ottpos  8192  smoiso  8308  ercnv  8669  ordiso2  9444  cantnfrescl  9605  cantnfp1lem3  9609  cantnflem1b  9615  cantnflem1  9618  cnfcom  9629  cnfcom3lem  9632  djulf1o  9841  djurf1o  9842  carden2  9916  cardeq0  10481  axpownd  10530  fpwwe2lem8  10567  fzen  13478  hasheq0  14304  incexc2  15780  divalglem4  16342  divalglem8  16346  divalgb  16350  sadadd  16413  sadass  16417  smuval2  16428  smumul  16439  isprm3  16629  vdwmc  16925  imasleval  17480  acsfn2  17600  invsym2  17701  yoniso  18222  pmtrfmvdn0  19368  dprd2d2  19952  cmpfi  23271  xkoinjcn  23550  tgpconncomp  23976  iscau3  25154  mbfimaopnlem  25532  ellimc3  25756  eldv  25775  eltayl  26243  atandm3  26764  noetasuplem4  27624  rmoxfrd  32395  opeldifid  32501  2ndpreima  32604  f1od2  32617  ordtconnlem1  33887  bnj1253  34980  usgrgt2cycl  35090  satfdm  35329  wl-dral1d  37492  wl-sb8eft  37512  wl-sb8et  37514  wl-equsb3  37517  wl-sb8eut  37539  wl-sb8eutv  37540  wl-issetft  37543  wl-ax11-lem8  37553  poimirlem2  37589  poimirlem16  37603  poimirlem18  37605  poimirlem21  37608  poimirlem22  37609  eqbrrdv2  38829  islpln5  39502  islvol5  39546  ntrneicls11  44052  radcnvrat  44276  trsbc  44503  iindif2f  45127  ichnreuop  47446  ichreuopeq  47447  pm5.32dav  48755  exp12bd  48757  reuxfr1dd  48768  aacllem  49763