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  3103  sspwb  5424  ssopab2bw  5526  ssopab2b  5528  wetrep  5648  imadif  6618  ssoprab2b  7483  eqoprab2bw  7484  tfinds2  7861  iiner  8792  fsetcdmex  8867  fiint  9299  dfac5lem5  10133  axpowndlem3  10611  uzind  12716  isprm5  16801  funcres2  17990  fthres2  18026  ipodrsima  18632  subrgdvds  20751  hausflim  24210  dvres2  26142  precsexlem11  28485  oncutlt  28532  uzsind  28673  axlowdimlem14  29415  atabs2i  32886  esum2dlem  34605  nn0prpw  36945  heibor1lem  38562  prter2  39757  dvelimf-o  39805  frege70  44776  frege72  44778  frege93  44799  frege110  44816  frege120  44826  pm11.71  45224  sbiota1  45261