Theorem 3imtr3g 284

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  aleximi  1799  sspwb  4947  ssopab2b  5031  wetrep  5136  imadif  6011  ssoprab2b  6754  suceloni  7055  tfinds2  7105  iiner  7862  fiint  8278  dfac5lem5  8988  axpowndlem3  9459  uzind  11507  isprm5  15466  funcres2  16605  fthres2  16639  ipodrsima  17212  subrgdvds  18842  hausflim  21832  dvres2  23721  axlowdimlem14  25880  atabs2i  29389  esum2dlem  30282  nn0prpw  32443  bj-hbext  32826  heibor1lem  33738  prter2  34485  dvelimf-o  34533  frege70  38544  frege72  38546  frege93  38567  frege110  38584  frege120  38594  pm11.71  38914  sbiota1  38952