Theorem 3imtr3g 287

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  aleximi  1927  sspwb  5108  ssopab2b  5198  wetrep  5305  imadif  6184  ssoprab2b  6946  suceloni  7247  tfinds2  7297  iiner  8057  fiint  8479  dfac5lem5  9236  axpowndlem3  9709  uzind  11759  isprm5  15752  funcres2  16872  fthres2  16906  ipodrsima  17480  subrgdvds  19112  hausflim  22113  dvres2  24017  axlowdimlem14  26192  atabs2i  29786  esum2dlem  30670  nn0prpw  32830  bj-hbext  33206  heibor1lem  34095  prter2  34902  dvelimf-o  34950  frege70  39009  frege72  39011  frege93  39032  frege110  39049  frege120  39059  pm11.71  39379  sbiota1  39416