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  1864  rexim  3107  sspwb  5421  ssopab2bw  5526  ssopab2b  5528  wetrep  5648  imadif  6635  ssoprab2b  7499  eqoprab2bw  7500  tfinds2  7885  iiner  8824  fsetcdmex  8899  fiint  9332  dfac5lem5  10219  axpowndlem3  10697  uzind  12804  isprm5  16898  funcres2  18088  fthres2  18124  ipodrsima  18730  subrgdvds  20853  hausflim  24315  dvres2  26247  precsexlem11  28618  oncutlt  28665  uzsind  28806  axlowdimlem14  29548  atabs2i  33019  esum2dlem  34780  nn0prpw  37244  heibor1lem  38889  prter2  40084  dvelimf-o  40132  frege70  45079  frege72  45081  frege93  45102  frege110  45119  frege120  45129  pm11.71  45527  sbiota1  45563  cocanss2  46067