Theorem 3bitr3g 221

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

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  con2bidc  861  sbal1yz  1977  sbal1  1978  dfsbcq2  2916  iindif2m  3888  opeqex  4179  rabxfrd  4398  eqbrrdv  4644  eqbrrdiv  4645  opelco2g  4715  opelcnvg  4727  ralrnmpt  5570  rexrnmpt  5571  fliftcnv  5704  eusvobj2  5768  f1od2  6140  ottposg  6160  ercnv  6458  exmidpw  6810  djuf1olem  6946  fzen  9854  fihasheq0  10572  divalgb  11658  isprm3  11835  eldvap  12859