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  1830  rexim  3093  sspwb  5469  ssopab2bw  5566  ssopab2b  5568  wetrep  5693  imadif  6662  ssoprab2b  7519  eqoprab2bw  7520  sucexeloniOLD  7846  suceloniOLD  7848  tfinds2  7901  iiner  8847  fsetcdmex  8921  fiint  9394  fiintOLD  9395  dfac5lem5  10196  axpowndlem3  10668  uzind  12735  isprm5  16754  funcres2  17962  fthres2  17999  ipodrsima  18611  subrgdvds  20614  hausflim  24010  dvres2  25967  precsexlem11  28259  uzsind  28409  axlowdimlem14  28988  atabs2i  32434  esum2dlem  34056  nn0prpw  36289  bj-hbext  36676  heibor1lem  37769  prter2  38837  dvelimf-o  38885  frege70  43895  frege72  43897  frege93  43918  frege110  43935  frege120  43945  pm11.71  44366  sbiota1  44403