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 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  aleximi  1859  rexim  3112  sspwb  5431  ssopab2bw  5533  ssopab2b  5535  wetrep  5655  imadif  6621  ssoprab2b  7480  eqoprab2bw  7481  tfinds2  7860  iiner  8787  fsetcdmex  8860  fiint  9286  dfac5lem5  10111  axpowndlem3  10584  uzind  12688  isprm5  16766  funcres2  17955  fthres2  17991  ipodrsima  18597  subrgdvds  20671  hausflim  24107  dvres2  26040  precsexlem11  28376  oncutlt  28423  uzsind  28564  axlowdimlem14  29246  atabs2i  32695  esum2dlem  34427  nn0prpw  36757  heibor1lem  38382  prter2  39579  dvelimf-o  39627  frege70  44585  frege72  44587  frege93  44608  frege110  44625  frege120  44635  pm11.71  45033  sbiota1  45070