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	bitrdi 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  870  sbal1yz  1994  sbal1  1995  dfsbcq2  2958  iindif2m  3940  opeqex  4234  rabxfrd  4454  eqbrrdv  4708  eqbrrdiv  4709  opelco2g  4779  opelcnvg  4791  ralrnmpt  5638  rexrnmpt  5639  fliftcnv  5774  eusvobj2  5839  f1od2  6214  ottposg  6234  ercnv  6534  exmidpw  6886  djuf1olem  7030  fzen  9999  fihasheq0  10728  divalgb  11884  isprm3  12072  eldvap  13445