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  1604  cbvexdvaw  2035  cbvexdw  2339  cbvexd  2410  cbvrexdva  3237  raleq  3320  rexeqbidvvOLD  3334  cbvrexdva2  3346  rexeqf  3351  cbvexeqsetf  3492  dfsbcq2  3793  unineq  4293  iindif2  5081  reusv2  5408  rabxfrd  5422  opeqex  5507  eqbrrdv  5805  eqbrrdiv  5806  opelco2g  5880  opelcnvg  5893  ralrnmptw  7113  ralrnmpt  7115  fliftcnv  7330  eusvobj2  7422  br1steqg  8034  br2ndeqg  8035  ottpos  8259  smoiso  8400  ercnv  8764  ordiso2  9552  cantnfrescl  9713  cantnfp1lem3  9717  cantnflem1b  9723  cantnflem1  9726  cnfcom  9737  cnfcom3lem  9740  djulf1o  9949  djurf1o  9950  carden2  10024  cardeq0  10589  axpownd  10638  fpwwe2lem8  10675  fzen  13577  hasheq0  14398  incexc2  15870  divalglem4  16429  divalglem8  16433  divalgb  16437  sadadd  16500  sadass  16504  smuval2  16515  smumul  16526  isprm3  16716  vdwmc  17011  imasleval  17587  acsfn2  17707  invsym2  17810  yoniso  18341  pmtrfmvdn0  19494  dprd2d2  20078  cmpfi  23431  xkoinjcn  23710  tgpconncomp  24136  iscau3  25325  mbfimaopnlem  25703  ellimc3  25928  eldv  25947  eltayl  26415  atandm3  26935  noetasuplem4  27795  rmoxfrd  32520  opeldifid  32618  2ndpreima  32722  f1od2  32738  ordtconnlem1  33884  bnj1253  35009  usgrgt2cycl  35114  satfdm  35353  wl-dral1d  37511  wl-sb8eft  37531  wl-sb8et  37533  wl-equsb3  37536  wl-sb8eut  37558  wl-sb8eutv  37559  wl-issetft  37562  wl-ax11-lem8  37572  poimirlem2  37608  poimirlem16  37622  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  eqbrrdv2  38844  islpln5  39517  islvol5  39561  ntrneicls11  44079  radcnvrat  44309  trsbc  44537  iindif2f  45102  ichnreuop  47396  ichreuopeq  47397  pm5.32dav  48642  exp12bd  48644  reuxfr1dd  48654  aacllem  49031