Theorem 3bitr3g 314

Description: More general version of 3bitr3i 302. 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 286	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	bitrdi 288	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  notbid  319  cador  1615  cbvexdvaw  2046  cbvexdw  2347  cbvexd  2416  cbvrexdva  3220  raleq  3294  cbvrexdva2  3316  rexeqf  3321  cbvexeqsetf  3446  dfsbcq2  3726  unineq  4216  iindif2  5006  reusv2  5332  rabxfrd  5346  opeqex  5439  eqbrrdv  5736  eqbrrdiv  5737  opelco2g  5809  opelcnvg  5822  ralrnmptw  7035  ralrnmpt  7037  fliftcnv  7255  eusvobj2  7348  br1steqg  7953  br2ndeqg  7954  ottpos  8176  smoiso  8292  ercnv  8655  ordiso2  9420  cantnfrescl  9588  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1  9601  cnfcom  9612  cnfcom3lem  9615  djulf1o  9827  djurf1o  9828  carden2  9902  cardeq0  10465  axpownd  10515  fpwwe2lem8  10552  fzen  13486  hasheq0  14316  incexc2  15794  divalglem4  16356  divalglem8  16360  divalgb  16364  sadadd  16427  sadass  16431  smuval2  16442  smumul  16453  isprm3  16643  vdwmc  16940  imasleval  17496  acsfn2  17620  invsym2  17721  yoniso  18242  pmtrfmvdn0  19428  dprd2d2  20012  cmpfi  23391  xkoinjcn  23670  tgpconncomp  24096  iscau3  25263  mbfimaopnlem  25640  ellimc3  25864  eldv  25883  eltayl  26343  atandm3  26860  noetasuplem4  27718  rmoxfrd  32580  opeldifid  32688  2ndpreima  32800  f1od2  32811  ordtconnlem1  34108  bnj1253  35199  usgrgt2cycl  35358  satfdm  35597  wl-dral1d  37902  wl-sb8eft  37922  wl-sb8et  37924  wl-equsb3  37927  wl-sb8eut  37949  wl-sb8eutv  37950  wl-issetft  37953  poimirlem2  37989  poimirlem16  38003  poimirlem18  38005  poimirlem21  38008  poimirlem22  38009  eqbrrdv2  39355  islpln5  40027  islvol5  40071  ntrneicls11  44534  radcnvrat  44758  trsbc  44984  iindif2f  45607  ichnreuop  47947  ichreuopeq  47948  pm5.32dav  49284  exp12bd  49286  reuxfr1dd  49297  aacllem  50291