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	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  1835  sspwb  5359  ssopab2bw  5453  ssopab2b  5455  wetrep  5573  imadif  6502  ssoprab2b  7322  eqoprab2bw  7323  suceloni  7635  tfinds2  7685  iiner  8536  fsetcdmex  8609  fiint  9021  dfac5lem5  9814  axpowndlem3  10286  uzind  12342  isprm5  16340  funcres2  17529  fthres2  17564  ipodrsima  18174  subrgdvds  19953  hausflim  23040  dvres2  24981  axlowdimlem14  27226  atabs2i  30665  esum2dlem  31960  nn0prpw  34439  bj-hbext  34819  heibor1lem  35894  prter2  36822  dvelimf-o  36870  frege70  41430  frege72  41432  frege93  41453  frege110  41470  frege120  41480  pm11.71  41904  sbiota1  41941