Theorem 3imtr3g 295

Description: More general version of 3imtr3i 291. 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 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  3172  sspwb  5365  ssopab2bw  5460  ssopab2b  5462  wetrep  5582  imadif  6518  ssoprab2b  7344  eqoprab2bw  7345  sucexeloni  7658  suceloniOLD  7660  tfinds2  7710  iiner  8578  fsetcdmex  8651  fiint  9091  dfac5lem5  9883  axpowndlem3  10355  uzind  12412  isprm5  16412  funcres2  17613  fthres2  17648  ipodrsima  18259  subrgdvds  20038  hausflim  23132  dvres2  25076  axlowdimlem14  27323  atabs2i  30764  esum2dlem  32060  nn0prpw  34512  bj-hbext  34892  heibor1lem  35967  prter2  36895  dvelimf-o  36943  frege70  41541  frege72  41543  frege93  41564  frege110  41581  frege120  41591  pm11.71  42015  sbiota1  42052