Theorem 3imtr3g 294

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  aleximi  1834  rexim  3086  sspwb  5442  ssopab2bw  5540  ssopab2b  5542  wetrep  5662  imadif  6621  ssoprab2b  7462  eqoprab2bw  7463  sucexeloniOLD  7781  suceloniOLD  7783  tfinds2  7836  iiner  8766  fsetcdmex  8840  fiint  9307  dfac5lem5  10104  axpowndlem3  10576  uzind  12636  isprm5  16626  funcres2  17830  fthres2  17865  ipodrsima  18476  subrgdvds  20326  hausflim  23414  dvres2  25358  axlowdimlem14  28078  atabs2i  31518  esum2dlem  32921  nn0prpw  35012  bj-hbext  35392  heibor1lem  36482  prter2  37556  dvelimf-o  37604  frege70  42455  frege72  42457  frege93  42478  frege110  42495  frege120  42505  pm11.71  42927  sbiota1  42964