Theorem 3bitr3g 302

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  notbid  307  cador  1695  cbvexd  2437  cbvexdva  2441  dfsbcq2  3591  unineq  4027  iindif2  4724  reusv2  5004  rabxfrd  5018  opeqex  5090  eqbrrdv  5358  eqbrrdiv  5359  opelco2g  5429  opelcnvg  5441  ralrnmpt  6512  fliftcnv  6705  eusvobj2  6787  br1steqg  7338  br2ndeqg  7339  ottpos  7515  smoiso  7613  ercnv  7918  ordiso2  8577  cantnfrescl  8738  cantnfp1lem3  8742  cantnflem1b  8748  cantnflem1  8751  cnfcom  8762  cnfcom3lem  8765  djulf1o  8939  djurf1o  8940  carden2  9014  cardeq0  9577  axpownd  9626  fpwwe2lem9  9663  fzen  12566  hasheq0  13357  incexc2  14778  divalglem4  15328  divalglem8  15332  divalgb  15336  divalgmodOLD  15339  sadadd  15398  sadass  15402  smuval2  15413  smumul  15424  isprm3  15604  vdwmc  15890  imasleval  16410  acsfn2  16532  invsym2  16631  yoniso  17134  pmtrfmvdn0  18090  dprd2d2  18652  cmpfi  21433  xkoinjcn  21712  tgpconncomp  22137  iscau3  23296  mbfimaopnlem  23643  ellimc3  23864  eldv  23883  eltayl  24335  atandm3  24827  rmoxfrdOLD  29672  rmoxfrd  29673  opeldifid  29751  2ndpreima  29826  f1od2  29840  ordtconnlem1  30311  bnj1253  31424  noetalem3  32203  wl-dral1d  33654  wl-sb8et  33670  wl-equsb3  33673  wl-sb8eut  33694  wl-ax11-lem8  33704  poimirlem2  33745  poimirlem16  33759  poimirlem18  33761  poimirlem21  33764  poimirlem22  33765  eqbrrdv2  34672  islpln5  35344  islvol5  35388  ntrneicls11  38915  radcnvrat  39040  trsbc  39276  aacllem  43079