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  1833  rexim  3073  sspwb  5388  ssopab2bw  5485  ssopab2b  5487  wetrep  5607  imadif  6565  ssoprab2b  7415  eqoprab2bw  7416  tfinds2  7794  iiner  8713  fsetcdmex  8787  fiint  9211  dfac5lem5  10018  axpowndlem3  10490  uzind  12565  isprm5  16618  funcres2  17805  fthres2  17841  ipodrsima  18447  subrgdvds  20501  hausflim  23896  dvres2  25840  precsexlem11  28155  onscutlt  28201  uzsind  28329  axlowdimlem14  28933  atabs2i  32382  esum2dlem  34105  nn0prpw  36367  bj-hbext  36754  heibor1lem  37848  prter2  38979  dvelimf-o  39027  frege70  44025  frege72  44027  frege93  44048  frege110  44065  frege120  44075  pm11.71  44489  sbiota1  44526