Theorem 3bitr3g 220

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  con2bidc  805  sbal1yz  1922  sbal1  1923  dfsbcq2  2832  iindif2m  3780  opeqex  4050  rabxfrd  4265  eqbrrdv  4503  eqbrrdiv  4504  opelco2g  4572  opelcnvg  4584  ralrnmpt  5404  rexrnmpt  5405  fliftcnv  5535  eusvobj2  5599  f1od2  5957  ottposg  5974  ercnv  6265  exmidpw  6576  djuf1olem  6689  fzen  9389  fihasheq0  10098  divalgb  10800  isprm3  10975