Theorem 3imtr3g 298

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  aleximi  1862  rexim  3106  sspwb  5430  ssopab2bw  5532  ssopab2b  5534  wetrep  5654  imadif  6620  ssoprab2b  7479  eqoprab2bw  7480  tfinds2  7856  iiner  8783  fsetcdmex  8856  fiint  9282  dfac5lem5  10116  axpowndlem3  10588  uzind  12692  isprm5  16770  funcres2  17959  fthres2  17995  ipodrsima  18601  subrgdvds  20694  hausflim  24147  dvres2  26080  precsexlem11  28419  oncutlt  28466  uzsind  28607  axlowdimlem14  29314  atabs2i  32763  esum2dlem  34491  nn0prpw  36862  heibor1lem  38488  prter2  39683  dvelimf-o  39731  frege70  44687  frege72  44689  frege93  44710  frege110  44727  frege120  44737  pm11.71  45135  sbiota1  45172