Theorem 3imtr3g 295

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  aleximi  1832  rexim  3070  sspwb  5392  ssopab2bw  5490  ssopab2b  5492  wetrep  5612  imadif  6566  ssoprab2b  7418  eqoprab2bw  7419  tfinds2  7797  iiner  8716  fsetcdmex  8790  fiint  9216  fiintOLD  9217  dfac5lem5  10021  axpowndlem3  10493  uzind  12568  isprm5  16618  funcres2  17805  fthres2  17841  ipodrsima  18447  subrgdvds  20471  hausflim  23866  dvres2  25811  precsexlem11  28124  onscutlt  28170  uzsind  28298  axlowdimlem14  28900  atabs2i  32346  esum2dlem  34065  nn0prpw  36307  bj-hbext  36694  heibor1lem  37799  prter2  38870  dvelimf-o  38918  frege70  43916  frege72  43918  frege93  43939  frege110  43956  frege120  43966  pm11.71  44380  sbiota1  44417