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  2369  cbvexd  2438  cbvrexdva  3244  raleq  3317  cbvrexdva2  3338  rexeqf  3343  cbvexeqsetf  3466  dfsbcq2  3742  unineq  4234  iindif2  5037  reusv2  5365  rabxfrd  5379  opeqex  5470  eqbrrdv  5769  eqbrrdiv  5770  opelco2g  5845  opelcnvg  5858  ralrnmptw  7092  ralrnmpt  7094  fliftcnv  7317  eusvobj2  7410  br1steqg  8021  br2ndeqg  8022  ottpos  8246  smoiso  8363  ercnv  8732  ordiso2  9502  cantnfrescl  9670  cantnfp1lem3  9674  cantnflem1b  9680  cantnflem1  9683  cnfcom  9694  cnfcom3lem  9697  djulf1o  9986  djurf1o  9987  carden2  10061  cardeq0  10629  axpownd  10679  fpwwe2lem8  10716  fzen  13667  hasheq0  14500  incexc2  16000  divalglem4  16559  divalglem8  16563  divalgb  16567  sadadd  16630  sadass  16634  smuval2  16645  smumul  16656  isprm3  16851  vdwmc  17149  imasleval  17706  acsfn2  17830  invsym2  17931  yoniso  18452  pmtrfmvdn0  19669  dprd2d2  20253  cmpfi  23719  xkoinjcn  23999  tgpconncomp  24425  iscau3  25592  mbfimaopnlem  25969  ellimc3  26192  eldv  26211  eltayl  26680  atandm3  27199  noetasuplem4  28086  dfprlng2  29418  rmoxfrd  33082  opeldifid  33186  2ndpreima  33294  f1od2  33304  ordtconnlem1  34549  bnj1253  35640  usgrgt2cycl  35888  satfdm  36113  wl-dral1d  38443  wl-sb8eft  38463  wl-sb8et  38465  wl-equsb3  38468  wl-sb8eut  38490  wl-sb8eutv  38491  wl-issetft  38494  poimirlem2  38520  poimirlem16  38534  poimirlem18  38536  poimirlem21  38539  poimirlem22  38540  eqbrrdv2  39900  islpln5  40572  islvol5  40616  ntrneicls11  45075  radcnvrat  45283  trsbc  45508  iindif2f  46144  ichnreuop  48523  ichreuopeq  48524  pm5.32rda  49873  exp12bd  49875  reuxfr1dd  49886  aacllem  50908