Theorem 3imtr3g 295

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  aleximi  1832  rexim  3087  sspwb  5454  ssopab2bw  5552  ssopab2b  5554  wetrep  5678  imadif  6650  ssoprab2b  7502  eqoprab2bw  7503  sucexeloniOLD  7830  suceloniOLD  7832  tfinds2  7885  iiner  8829  fsetcdmex  8903  fiint  9366  fiintOLD  9367  dfac5lem5  10167  axpowndlem3  10639  uzind  12710  isprm5  16744  funcres2  17943  fthres2  17979  ipodrsima  18586  subrgdvds  20586  hausflim  23989  dvres2  25947  precsexlem11  28241  uzsind  28391  axlowdimlem14  28970  atabs2i  32421  esum2dlem  34093  nn0prpw  36324  bj-hbext  36711  heibor1lem  37816  prter2  38882  dvelimf-o  38930  frege70  43946  frege72  43948  frege93  43969  frege110  43986  frege120  43996  pm11.71  44416  sbiota1  44453