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  2020  sbal1  2021  dfsbcq2  2992  iindif2m  3985  opeqex  4283  rabxfrd  4505  eqbrrdv  4761  eqbrrdiv  4762  opelco2g  4835  opelcnvg  4847  ralrnmpt  5707  rexrnmpt  5708  fliftcnv  5845  eusvobj2  5911  f1od2  6302  ottposg  6322  ercnv  6622  exmidpw  6978  djuf1olem  7128  fzen  10135  fihasheq0  10902  divalgb  12107  isprm3  12311  eldvap  15002