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  1587  cbvexdva  2319  dfsbcq2  3471  unineq  3910  iindif2  4621  reusv2  4904  rabxfrd  4919  opeqex  4991  eqbrrdv  5251  eqbrrdiv  5252  opelco2g  5322  opelcnvg  5334  ralrnmpt  6408  fliftcnv  6601  eusvobj2  6683  br1steqg  7232  br2ndeqg  7233  ottpos  7407  smoiso  7504  ercnv  7808  ordiso2  8461  cantnfrescl  8611  cantnfp1lem3  8615  cantnflem1b  8621  cantnflem1  8624  cnfcom  8635  cnfcom3lem  8638  carden2  8851  cardeq0  9412  axpownd  9461  fpwwe2lem9  9498  fzen  12396  hasheq0  13192  incexc2  14614  divalglem4  15166  divalglem8  15170  divalgb  15174  divalgmodOLD  15177  sadadd  15236  sadass  15240  smuval2  15251  smumul  15262  isprm3  15443  vdwmc  15729  imasleval  16248  acsfn2  16371  invsym2  16470  yoniso  16972  pmtrfmvdn0  17928  dprd2d2  18489  cmpfi  21259  xkoinjcn  21538  tgpconncomp  21963  iscau3  23122  mbfimaopnlem  23467  ellimc3  23688  eldv  23707  eltayl  24159  atandm3  24650  rmoxfrdOLD  29459  rmoxfrd  29460  opeldifid  29538  2ndpreima  29613  f1od2  29627  ordtconnlem1  30098  bnj1253  31211  noetalem3  31990  wl-dral1d  33448  wl-sb8et  33464  wl-equsb3  33467  wl-sb8eut  33489  wl-ax11-lem8  33499  poimirlem2  33541  poimirlem16  33555  poimirlem18  33557  poimirlem21  33560  poimirlem22  33561  eqbrrdv2  34467  islpln5  35139  islvol5  35183  ntrneicls11  38705  radcnvrat  38830  trsbc  39067  aacllem  42875