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  3079  sspwb  5406  ssopab2bw  5505  ssopab2b  5507  wetrep  5627  imadif  6586  ssoprab2b  7439  eqoprab2bw  7440  tfinds2  7818  iiner  8740  fsetcdmex  8814  fiint  9241  dfac5lem5  10051  axpowndlem3  10524  uzind  12598  isprm5  16648  funcres2  17836  fthres2  17872  ipodrsima  18478  subrgdvds  20536  hausflim  23942  dvres2  25886  precsexlem11  28230  oncutlt  28277  uzsind  28418  axlowdimlem14  29046  atabs2i  32496  esum2dlem  34276  nn0prpw  36545  heibor1lem  38089  prter2  39286  dvelimf-o  39334  frege70  44318  frege72  44320  frege93  44341  frege110  44358  frege120  44368  pm11.71  44782  sbiota1  44819