Theorem 3imtr3g 297

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  aleximi  1854  rexim  3105  sspwb  5418  ssopab2bw  5520  ssopab2b  5522  wetrep  5642  imadif  6607  ssoprab2b  7467  eqoprab2bw  7468  tfinds2  7846  iiner  8773  fsetcdmex  8846  fiint  9273  dfac5lem5  10085  axpowndlem3  10559  uzind  12667  isprm5  16744  funcres2  17933  fthres2  17969  ipodrsima  18575  subrgdvds  20638  hausflim  24043  dvres2  25976  precsexlem11  28312  oncutlt  28359  uzsind  28500  axlowdimlem14  29158  atabs2i  32607  esum2dlem  34391  nn0prpw  36688  heibor1lem  38313  prter2  39510  dvelimf-o  39558  frege70  44514  frege72  44516  frege93  44537  frege110  44554  frege120  44564  pm11.71  44978  sbiota1  45015