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 242	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	imbitrdi 250	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  aleximi  1835  rexim  3088  sspwb  5450  ssopab2bw  5548  ssopab2b  5550  wetrep  5670  imadif  6633  ssoprab2b  7478  eqoprab2bw  7479  sucexeloniOLD  7798  suceloniOLD  7800  tfinds2  7853  iiner  8783  fsetcdmex  8857  fiint  9324  dfac5lem5  10122  axpowndlem3  10594  uzind  12654  isprm5  16644  funcres2  17848  fthres2  17883  ipodrsima  18494  subrgdvds  20333  hausflim  23485  dvres2  25429  precsexlem11  27663  axlowdimlem14  28213  atabs2i  31655  esum2dlem  33090  nn0prpw  35208  bj-hbext  35588  heibor1lem  36677  prter2  37751  dvelimf-o  37799  frege70  42684  frege72  42686  frege93  42707  frege110  42724  frege120  42734  pm11.71  43156  sbiota1  43193