Theorem 3bitr3g 297

Description: More general version of 3bitr3i 285. 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	syl5bbr 269	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	syl6bb 271	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 191

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 192

This theorem is referenced by:  notbid  303  cador  1535  equequ2OLD  1904  dfsbcq2  3294  unineq  3720  iindif2  4376  reusv2  4648  rabxfrd  4662  opeqex  4733  eqbrrdv  4979  eqbrrdiv  4980  opelco2g  5049  opelcnvg  5062  ralrnmpt  6098  fliftcnv  6275  eusvobj2  6356  ottpos  7060  smoiso  7158  ercnv  7461  ordiso2  8113  cantnfrescl  8266  cantnfp1lem3  8270  cantnflem1b  8276  cantnflem1  8279  cnfcom  8290  cnfcom3lem  8293  carden2  8506  cardeq0  9062  axpownd  9111  fpwwe2lem9  9148  fzen  11912  hasheq0  12662  incexc2  14056  divalglem4  14537  divalglem8  14542  divalgb  14547  divalgmod  14549  sadadd  14603  sadass  14607  smuval2  14618  smumul  14629  isprm3  14795  vdwmc  15090  imasleval  15612  acsfn2  15735  invsym2  15834  yoniso  16336  pmtrfmvdn0  17264  dprd2d2  17837  cmpfi  20580  xkoinjcn  20859  tgpconcomp  21285  iscau3  22407  mbfimaopnlem  22772  ellimc3  22995  eldv  23014  eltayl  23476  atandm3  23965  el2wlkonot  25757  el2spthonot  25758  rmoxfrdOLD  28289  rmoxfrd  28290  opeldifid  28368  2ndpreima  28445  f1od2  28465  ordtconlem1  28885  bnj1253  29978  wl-dral1d  32095  wl-sb8et  32112  wl-equsb3  32115  wl-sb8eut  32137  wl-ax11-lem8  32147  poimirlem2  32180  poimirlem16  32194  poimirlem18  32196  poimirlem21  32199  poimirlem22  32200  eqbrrdv2  32668  islpln5  33340  islvol5  33384  ntrneicls11  36901  radcnvrat  37020  trsbc  37257  aacllem  41727