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  1834  rexim  3078  sspwb  5398  ssopab2bw  5496  ssopab2b  5498  wetrep  5618  imadif  6577  ssoprab2b  7429  eqoprab2bw  7430  tfinds2  7808  iiner  8730  fsetcdmex  8804  fiint  9231  dfac5lem5  10041  axpowndlem3  10514  uzind  12588  isprm5  16638  funcres2  17826  fthres2  17862  ipodrsima  18468  subrgdvds  20523  hausflim  23929  dvres2  25873  precsexlem11  28217  oncutlt  28264  uzsind  28405  axlowdimlem14  29032  atabs2i  32481  esum2dlem  34251  nn0prpw  36519  bj-hbext  36913  heibor1lem  38012  prter2  39209  dvelimf-o  39257  frege70  44241  frege72  44243  frege93  44264  frege110  44281  frege120  44291  pm11.71  44705  sbiota1  44742