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  5404  ssopab2bw  5502  ssopab2b  5504  wetrep  5624  imadif  6584  ssoprab2b  7438  eqoprab2bw  7439  sucexeloniOLD  7766  tfinds2  7820  iiner  8739  fsetcdmex  8813  fiint  9253  fiintOLD  9254  dfac5lem5  10056  axpowndlem3  10528  uzind  12602  isprm5  16653  funcres2  17840  fthres2  17876  ipodrsima  18482  subrgdvds  20506  hausflim  23901  dvres2  25846  precsexlem11  28159  onscutlt  28205  uzsind  28333  axlowdimlem14  28935  atabs2i  32381  esum2dlem  34075  nn0prpw  36304  bj-hbext  36691  heibor1lem  37796  prter2  38867  dvelimf-o  38915  frege70  43915  frege72  43917  frege93  43938  frege110  43955  frege120  43965  pm11.71  44379  sbiota1  44416