Theorem 3imtr3g 298

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  aleximi  1833  sspwb  5307  ssopab2bw  5399  ssopab2b  5401  wetrep  5512  imadif  6408  ssoprab2b  7202  eqoprab2bw  7203  suceloni  7508  tfinds2  7558  iiner  8352  fiint  8779  dfac5lem5  9538  axpowndlem3  10010  uzind  12062  isprm5  16041  funcres2  17160  fthres2  17194  ipodrsima  17767  subrgdvds  19542  hausflim  22586  dvres2  24515  axlowdimlem14  26749  atabs2i  30185  esum2dlem  31461  nn0prpw  33784  bj-hbext  34157  heibor1lem  35247  prter2  36177  dvelimf-o  36225  frege70  40634  frege72  40636  frege93  40657  frege110  40674  frege120  40684  pm11.71  41101  sbiota1  41138