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  1865  rexim  3104  sspwb  5417  ssopab2bw  5522  ssopab2b  5524  wetrep  5644  imadif  6624  ssoprab2b  7489  eqoprab2bw  7490  tfinds2  7875  iiner  8810  fsetcdmex  8885  fiint  9318  dfac5lem5  10206  axpowndlem3  10684  uzind  12791  isprm5  16883  funcres2  18073  fthres2  18109  ipodrsima  18715  subrgdvds  20838  hausflim  24300  dvres2  26232  precsexlem11  28603  oncutlt  28650  uzsind  28791  axlowdimlem14  29533  atabs2i  33004  esum2dlem  34724  nn0prpw  37111  heibor1lem  38743  prter2  39938  dvelimf-o  39986  frege70  44932  frege72  44934  frege93  44955  frege110  44972  frege120  44982  pm11.71  45380  sbiota1  45417  cocanss2  45921