Theorem 3bitr3g 316

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  notbid  321  cador  1641  cbvexdvaw  2072  cbvexdw  2368  cbvexd  2437  cbvrexdva  3243  raleq  3316  cbvrexdva2  3337  rexeqf  3342  cbvexeqsetf  3465  dfsbcq2  3742  unineq  4234  iindif2  5037  reusv2  5368  rabxfrd  5382  opeqex  5475  eqbrrdv  5773  eqbrrdiv  5774  opelco2g  5847  opelcnvg  5860  ralrnmptw  7087  ralrnmpt  7089  fliftcnv  7312  eusvobj2  7405  br1steqg  8008  br2ndeqg  8009  ottpos  8234  smoiso  8351  ercnv  8718  ordiso2  9487  cantnfrescl  9655  cantnfp1lem3  9659  cantnflem1b  9665  cantnflem1  9668  cnfcom  9679  cnfcom3lem  9682  djulf1o  9917  djurf1o  9918  carden2  9992  cardeq0  10560  axpownd  10610  fpwwe2lem8  10647  fzen  13595  hasheq0  14427  incexc2  15927  divalglem4  16486  divalglem8  16490  divalgb  16494  sadadd  16557  sadass  16561  smuval2  16572  smumul  16583  isprm3  16773  vdwmc  17070  imasleval  17627  acsfn2  17751  invsym2  17852  yoniso  18373  pmtrfmvdn0  19589  dprd2d2  20173  cmpfi  23633  xkoinjcn  23913  tgpconncomp  24339  iscau3  25506  mbfimaopnlem  25883  ellimc3  26106  eldv  26125  eltayl  26596  atandm3  27115  noetasuplem4  27972  dfprlng2  29304  rmoxfrd  32968  opeldifid  33072  2ndpreima  33180  f1od2  33190  ordtconnlem1  34434  bnj1253  35526  usgrgt2cycl  35723  satfdm  35948  wl-dral1d  38294  wl-sb8eft  38314  wl-sb8et  38316  wl-equsb3  38319  wl-sb8eut  38341  wl-sb8eutv  38342  wl-issetft  38345  poimirlem2  38371  poimirlem16  38385  poimirlem18  38387  poimirlem21  38390  poimirlem22  38391  eqbrrdv2  39736  islpln5  40408  islvol5  40452  ntrneicls11  44930  radcnvrat  45138  trsbc  45363  iindif2f  45992  ichnreuop  48372  ichreuopeq  48373  pm5.32dav  49722  exp12bd  49724  reuxfr1dd  49735  aacllem  50772