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  3075  sspwb  5395  ssopab2bw  5493  ssopab2b  5495  wetrep  5615  imadif  6574  ssoprab2b  7425  eqoprab2bw  7426  tfinds2  7804  iiner  8724  fsetcdmex  8798  fiint  9225  dfac5lem5  10035  axpowndlem3  10508  uzind  12582  isprm5  16632  funcres2  17820  fthres2  17856  ipodrsima  18462  subrgdvds  20517  hausflim  23923  dvres2  25867  precsexlem11  28185  onscutlt  28232  uzsind  28363  axlowdimlem14  28977  atabs2i  32426  esum2dlem  34198  nn0prpw  36466  bj-hbext  36854  heibor1lem  37949  prter2  39080  dvelimf-o  39128  frege70  44116  frege72  44118  frege93  44139  frege110  44156  frege120  44166  pm11.71  44580  sbiota1  44617