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  3078  sspwb  5401  ssopab2bw  5502  ssopab2b  5504  wetrep  5624  imadif  6582  ssoprab2b  7436  eqoprab2bw  7437  tfinds2  7815  iiner  8736  fsetcdmex  8810  fiint  9237  dfac5lem5  10049  axpowndlem3  10522  uzind  12621  isprm5  16677  funcres2  17865  fthres2  17901  ipodrsima  18507  subrgdvds  20563  hausflim  23946  dvres2  25879  precsexlem11  28209  oncutlt  28256  uzsind  28397  axlowdimlem14  29024  atabs2i  32473  esum2dlem  34236  nn0prpw  36505  heibor1lem  38130  prter2  39327  dvelimf-o  39375  frege70  44360  frege72  44362  frege93  44383  frege110  44400  frege120  44410  pm11.71  44824  sbiota1  44861