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  1829  rexim  3085  sspwb  5460  ssopab2bw  5557  ssopab2b  5559  wetrep  5682  imadif  6652  ssoprab2b  7502  eqoprab2bw  7503  sucexeloniOLD  7830  suceloniOLD  7832  tfinds2  7885  iiner  8828  fsetcdmex  8902  fiint  9364  fiintOLD  9365  dfac5lem5  10165  axpowndlem3  10637  uzind  12708  isprm5  16741  funcres2  17949  fthres2  17986  ipodrsima  18599  subrgdvds  20603  hausflim  24005  dvres2  25962  precsexlem11  28256  uzsind  28406  axlowdimlem14  28985  atabs2i  32431  esum2dlem  34073  nn0prpw  36306  bj-hbext  36693  heibor1lem  37796  prter2  38863  dvelimf-o  38911  frege70  43923  frege72  43925  frege93  43946  frege110  43963  frege120  43973  pm11.71  44393  sbiota1  44430