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  5398  ssopab2bw  5497  ssopab2b  5499  wetrep  5619  imadif  6578  ssoprab2b  7431  eqoprab2bw  7432  tfinds2  7810  iiner  8731  fsetcdmex  8805  fiint  9232  dfac5lem5  10044  axpowndlem3  10517  uzind  12616  isprm5  16672  funcres2  17860  fthres2  17896  ipodrsima  18502  subrgdvds  20558  hausflim  23960  dvres2  25893  precsexlem11  28227  oncutlt  28274  uzsind  28415  axlowdimlem14  29042  atabs2i  32492  esum2dlem  34256  nn0prpw  36525  heibor1lem  38148  prter2  39345  dvelimf-o  39393  frege70  44382  frege72  44384  frege93  44405  frege110  44422  frege120  44432  pm11.71  44846  sbiota1  44883