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  1828  sspwb  5333  ssopab2bw  5426  ssopab2b  5428  wetrep  5542  imadif  6432  ssoprab2b  7217  eqoprab2bw  7218  suceloni  7522  tfinds2  7572  iiner  8363  fiint  8789  dfac5lem5  9547  axpowndlem3  10015  uzind  12068  isprm5  16045  funcres2  17162  fthres2  17196  ipodrsima  17769  subrgdvds  19543  hausflim  22583  dvres2  24504  axlowdimlem14  26735  atabs2i  30173  esum2dlem  31346  nn0prpw  33666  bj-hbext  34039  heibor1lem  35081  prter2  36011  dvelimf-o  36059  frege70  40272  frege72  40274  frege93  40295  frege110  40312  frege120  40322  pm11.71  40722  sbiota1  40759