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  1826  rexim  3076  sspwb  5451  ssopab2bw  5549  ssopab2b  5551  wetrep  5671  imadif  6638  ssoprab2b  7489  eqoprab2bw  7490  sucexeloniOLD  7814  suceloniOLD  7816  tfinds2  7869  iiner  8808  fsetcdmex  8882  fiint  9350  dfac5lem5  10152  axpowndlem3  10624  uzind  12687  isprm5  16681  funcres2  17887  fthres2  17924  ipodrsima  18536  subrgdvds  20537  hausflim  23929  dvres2  25885  precsexlem11  28165  axlowdimlem14  28838  atabs2i  32284  esum2dlem  33842  nn0prpw  35938  bj-hbext  36318  heibor1lem  37413  prter2  38483  dvelimf-o  38531  frege70  43505  frege72  43507  frege93  43528  frege110  43545  frege120  43555  pm11.71  43976  sbiota1  44013

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »