Theorem 3bitr3g 222

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  con2bidc  876  sbal1yz  2028  sbal1  2029  dfsbcq2  3000  iindif2m  3994  opeqex  4292  rabxfrd  4514  eqbrrdv  4770  eqbrrdiv  4771  opelco2g  4844  opelcnvg  4856  ralrnmpt  5716  rexrnmpt  5717  fliftcnv  5854  eusvobj2  5920  f1od2  6311  ottposg  6331  ercnv  6631  exmidpw  6987  djuf1olem  7137  fzen  10147  fihasheq0  10919  divalgb  12155  isprm3  12359  eldvap  15072