Theorem 3imtr3g 297

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  aleximi  1832  sspwb  5344  ssopab2bw  5436  ssopab2b  5438  wetrep  5550  imadif  6440  ssoprab2b  7225  eqoprab2bw  7226  suceloni  7530  tfinds2  7580  iiner  8371  fiint  8797  dfac5lem5  9555  axpowndlem3  10023  uzind  12077  isprm5  16053  funcres2  17170  fthres2  17204  ipodrsima  17777  subrgdvds  19551  hausflim  22591  dvres2  24512  axlowdimlem14  26743  atabs2i  30181  esum2dlem  31353  nn0prpw  33673  bj-hbext  34046  heibor1lem  35089  prter2  36019  dvelimf-o  36067  frege70  40286  frege72  40288  frege93  40309  frege110  40326  frege120  40336  pm11.71  40736  sbiota1  40773