Theorem 3imtr3g 297

Description: More general version of 3imtr3i 293. 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 245	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	imbitrdi 253	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  aleximi  1846  rexim  3097  sspwb  5410  ssopab2bw  5511  ssopab2b  5513  wetrep  5633  imadif  6594  ssoprab2b  7454  eqoprab2bw  7455  tfinds2  7833  iiner  8759  fsetcdmex  8833  fiint  9260  dfac5lem5  10073  axpowndlem3  10547  uzind  12655  isprm5  16718  funcres2  17907  fthres2  17943  ipodrsima  18549  subrgdvds  20608  hausflim  24014  dvres2  25947  precsexlem11  28280  oncutlt  28327  uzsind  28468  axlowdimlem14  29095  atabs2i  32544  esum2dlem  34343  nn0prpw  36631  heibor1lem  38256  prter2  39453  dvelimf-o  39501  frege70  44457  frege72  44459  frege93  44480  frege110  44497  frege120  44507  pm11.71  44921  sbiota1  44958