Theorem 3imtr3g 298

Description: More general version of 3imtr3i 294. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)

Hypotheses

Ref	Expression
3imtr3g.1	⊢ (𝜑 → (𝜓 → 𝜒))
3imtr3g.2	⊢ (𝜓 ↔ 𝜃)
3imtr3g.3	⊢ (𝜒 ↔ 𝜏)

Assertion

Ref	Expression
3imtr3g	⊢ (𝜑 → (𝜃 → 𝜏))

Proof of Theorem 3imtr3g

Step	Hyp	Ref	Expression
1		3imtr3g.2	. . 3 ⊢ (𝜓 ↔ 𝜃)
2		3imtr3g.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	biimtrrid 246	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	imbitrdi 254	1 ⊢ (𝜑 → (𝜃 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  aleximi  1865  rexim  3108  sspwb  5432  ssopab2bw  5534  ssopab2b  5536  wetrep  5656  imadif  6624  ssoprab2b  7488  eqoprab2bw  7489  tfinds2  7866  iiner  8793  fsetcdmex  8866  fiint  9293  dfac5lem5  10127  axpowndlem3  10603  uzind  12708  isprm5  16792  funcres2  17981  fthres2  18017  ipodrsima  18623  subrgdvds  20739  hausflim  24193  dvres2  26126  precsexlem11  28465  oncutlt  28512  uzsind  28653  axlowdimlem14  29364  atabs2i  32829  esum2dlem  34550  nn0prpw  36895  heibor1lem  38522  prter2  39717  dvelimf-o  39765  frege70  44736  frege72  44738  frege93  44759  frege110  44776  frege120  44786  pm11.71  45184  sbiota1  45221