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  308  cador  1547  equequ2OLD  1955  cbvexdva  2283  dfsbcq2  3438  unineq  3877  iindif2  4589  reusv2  4874  rabxfrd  4889  opeqex  4962  eqbrrdv  5217  eqbrrdiv  5218  opelco2g  5289  opelcnvg  5302  ralrnmpt  6368  fliftcnv  6561  eusvobj2  6643  ottpos  7362  smoiso  7459  ercnv  7763  ordiso2  8420  cantnfrescl  8573  cantnfp1lem3  8577  cantnflem1b  8583  cantnflem1  8586  cnfcom  8597  cnfcom3lem  8600  carden2  8813  cardeq0  9374  axpownd  9423  fpwwe2lem9  9460  fzen  12358  hasheq0  13154  incexc2  14570  divalglem4  15119  divalglem8  15123  divalgb  15127  divalgmodOLD  15130  sadadd  15189  sadass  15193  smuval2  15204  smumul  15215  isprm3  15396  vdwmc  15682  imasleval  16201  acsfn2  16324  invsym2  16423  yoniso  16925  pmtrfmvdn0  17882  dprd2d2  18443  cmpfi  21211  xkoinjcn  21490  tgpconncomp  21916  iscau3  23076  mbfimaopnlem  23422  ellimc3  23643  eldv  23662  eltayl  24114  atandm3  24605  rmoxfrdOLD  29332  rmoxfrd  29333  opeldifid  29412  2ndpreima  29485  f1od2  29499  ordtconnlem1  29970  bnj1253  31085  br1steqg  31672  br2ndeqg  31673  noetalem3  31865  wl-dral1d  33318  wl-sb8et  33334  wl-equsb3  33337  wl-sb8eut  33359  wl-ax11-lem8  33369  poimirlem2  33411  poimirlem16  33425  poimirlem18  33427  poimirlem21  33430  poimirlem22  33431  eqbrrdv2  34148  islpln5  34821  islvol5  34865  ntrneicls11  38388  radcnvrat  38513  trsbc  38750  aacllem  42547