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	biimtrrid 243	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr3g.3	. 2 ⊢ (𝜒 ↔ 𝜏)
5	3, 4	imbitrdi 251	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  aleximi  1832  rexim  3077  sspwb  5424  ssopab2bw  5522  ssopab2b  5524  wetrep  5647  imadif  6620  ssoprab2b  7476  eqoprab2bw  7477  sucexeloniOLD  7804  suceloniOLD  7806  tfinds2  7859  iiner  8803  fsetcdmex  8877  fiint  9338  fiintOLD  9339  dfac5lem5  10141  axpowndlem3  10613  uzind  12685  isprm5  16726  funcres2  17911  fthres2  17947  ipodrsima  18551  subrgdvds  20546  hausflim  23919  dvres2  25865  precsexlem11  28171  onscutlt  28217  uzsind  28345  axlowdimlem14  28934  atabs2i  32383  esum2dlem  34123  nn0prpw  36341  bj-hbext  36728  heibor1lem  37833  prter2  38899  dvelimf-o  38947  frege70  43957  frege72  43959  frege93  43980  frege110  43997  frege120  44007  pm11.71  44421  sbiota1  44458