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  3070  sspwb  5409  ssopab2bw  5507  ssopab2b  5509  wetrep  5631  imadif  6600  ssoprab2b  7458  eqoprab2bw  7459  sucexeloniOLD  7786  tfinds2  7840  iiner  8762  fsetcdmex  8836  fiint  9277  fiintOLD  9278  dfac5lem5  10080  axpowndlem3  10552  uzind  12626  isprm5  16677  funcres2  17860  fthres2  17896  ipodrsima  18500  subrgdvds  20495  hausflim  23868  dvres2  25813  precsexlem11  28119  onscutlt  28165  uzsind  28293  axlowdimlem14  28882  atabs2i  32331  esum2dlem  34082  nn0prpw  36311  bj-hbext  36698  heibor1lem  37803  prter2  38874  dvelimf-o  38922  frege70  43922  frege72  43924  frege93  43945  frege110  43962  frege120  43972  pm11.71  44386  sbiota1  44423