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  1609  cbvexdvaw  2040  cbvexdw  2341  cbvexd  2410  cbvrexdva  3214  raleq  3290  rexeqbidvvOLD  3304  cbvrexdva2  3316  rexeqf  3323  cbvexeqsetf  3452  dfsbcq2  3740  unineq  4237  iindif2  5029  reusv2  5345  rabxfrd  5359  opeqex  5443  eqbrrdv  5739  eqbrrdiv  5740  opelco2g  5813  opelcnvg  5826  ralrnmptw  7036  ralrnmpt  7038  fliftcnv  7254  eusvobj2  7347  br1steqg  7952  br2ndeqg  7953  ottpos  8175  smoiso  8291  ercnv  8652  ordiso2  9412  cantnfrescl  9577  cantnfp1lem3  9581  cantnflem1b  9587  cantnflem1  9590  cnfcom  9601  cnfcom3lem  9604  djulf1o  9816  djurf1o  9817  carden2  9891  cardeq0  10454  axpownd  10503  fpwwe2lem8  10540  fzen  13448  hasheq0  14277  incexc2  15752  divalglem4  16314  divalglem8  16318  divalgb  16322  sadadd  16385  sadass  16389  smuval2  16400  smumul  16411  isprm3  16601  vdwmc  16897  imasleval  17453  acsfn2  17577  invsym2  17678  yoniso  18199  pmtrfmvdn0  19382  dprd2d2  19966  cmpfi  23343  xkoinjcn  23622  tgpconncomp  24048  iscau3  25225  mbfimaopnlem  25603  ellimc3  25827  eldv  25846  eltayl  26314  atandm3  26835  noetasuplem4  27695  rmoxfrd  32493  opeldifid  32600  2ndpreima  32713  f1od2  32726  ordtconnlem1  34009  bnj1253  35101  usgrgt2cycl  35246  satfdm  35485  wl-dral1d  37648  wl-sb8eft  37668  wl-sb8et  37670  wl-equsb3  37673  wl-sb8eut  37695  wl-sb8eutv  37696  wl-issetft  37699  poimirlem2  37735  poimirlem16  37749  poimirlem18  37751  poimirlem21  37754  poimirlem22  37755  eqbrrdv2  39035  islpln5  39707  islvol5  39751  ntrneicls11  44247  radcnvrat  44471  trsbc  44697  iindif2f  45320  ichnreuop  47634  ichreuopeq  47635  pm5.32dav  48955  exp12bd  48957  reuxfr1dd  48968  aacllem  49962