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  3071  sspwb  5412  ssopab2bw  5510  ssopab2b  5512  wetrep  5634  imadif  6603  ssoprab2b  7461  eqoprab2bw  7462  sucexeloniOLD  7789  tfinds2  7843  iiner  8765  fsetcdmex  8839  fiint  9284  fiintOLD  9285  dfac5lem5  10087  axpowndlem3  10559  uzind  12633  isprm5  16684  funcres2  17867  fthres2  17903  ipodrsima  18507  subrgdvds  20502  hausflim  23875  dvres2  25820  precsexlem11  28126  onscutlt  28172  uzsind  28300  axlowdimlem14  28889  atabs2i  32338  esum2dlem  34089  nn0prpw  36318  bj-hbext  36705  heibor1lem  37810  prter2  38881  dvelimf-o  38929  frege70  43929  frege72  43931  frege93  43952  frege110  43969  frege120  43979  pm11.71  44393  sbiota1  44430