Theorem 3imtr3g 296

Description: More general version of 3imtr3i 292. 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 244	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	imbitrdi 252	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  aleximi  1839  rexim  3080  sspwb  5389  ssopab2bw  5490  ssopab2b  5492  wetrep  5612  imadif  6570  ssoprab2b  7426  eqoprab2bw  7427  tfinds2  7805  iiner  8727  fsetcdmex  8801  fiint  9228  dfac5lem5  10041  axpowndlem3  10514  uzind  12613  isprm5  16669  funcres2  17857  fthres2  17893  ipodrsima  18499  subrgdvds  20559  hausflim  23965  dvres2  25898  precsexlem11  28228  oncutlt  28275  uzsind  28416  axlowdimlem14  29043  atabs2i  32492  esum2dlem  34285  nn0prpw  36560  heibor1lem  38185  prter2  39382  dvelimf-o  39430  frege70  44386  frege72  44388  frege93  44409  frege110  44426  frege120  44436  pm11.71  44850  sbiota1  44887