Theorem 3imtr3g 283

Description: More general version of 3imtr3i 279. 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	syl5bir 232	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	syl6ib 240	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  aleximi  1749  sspwb  4844  ssopab2b  4927  wetrep  5031  imadif  5887  ssoprab2b  6610  suceloni  6905  tfinds2  6955  iiner  7706  fiint  8122  dfac5lem5  8833  axpowndlem3  9300  uzind  11345  isprm5  15257  funcres2  16381  fthres2  16415  ipodrsima  16988  subrgdvds  18617  hausflim  21595  dvres2  23482  axlowdimlem14  25635  atabs2i  28645  esum2dlem  29481  nn0prpw  31488  bj-hbext  31888  heibor1lem  32778  prter2  33184  dvelimf-o  33232  frege70  37247  frege72  37249  frege93  37270  frege110  37287  frege120  37297  pm11.71  37619  sbiota1  37657