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	imbitrdi 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  3087  sspwb  5449  ssopab2bw  5547  ssopab2b  5549  wetrep  5669  imadif  6632  ssoprab2b  7477  eqoprab2bw  7478  sucexeloniOLD  7797  suceloniOLD  7799  tfinds2  7852  iiner  8782  fsetcdmex  8856  fiint  9323  dfac5lem5  10121  axpowndlem3  10593  uzind  12653  isprm5  16643  funcres2  17847  fthres2  17882  ipodrsima  18493  subrgdvds  20332  hausflim  23484  dvres2  25428  precsexlem11  27660  axlowdimlem14  28210  atabs2i  31650  esum2dlem  33085  nn0prpw  35203  bj-hbext  35583  heibor1lem  36672  prter2  37746  dvelimf-o  37794  frege70  42674  frege72  42676  frege93  42697  frege110  42714  frege120  42724  pm11.71  43146  sbiota1  43183