Theorem 3imtr3g 554

Description: More general version of 3imtr3 218. Useful for converting definitions in a formula.

Hypotheses

Ref	Expression
3imtr3g.1	⊢ (φ → (ψ → χ))
3imtr3g.2	⊢ (ψ ↔ θ)
3imtr3g.3	⊢ (χ ↔ τ)

Assertion

Ref	Expression
3imtr3g	⊢ (φ → (θ → τ))

Proof of Theorem 3imtr3g

Step	Hyp	Ref	Expression
1		3imtr3g.1	. . . 4 ⊢ (φ → (ψ → χ))
2	1	imp 350	. . 3 ⊢ ((φ ⋀ ψ) → χ)
3		3imtr3g.2	. . . 4 ⊢ (ψ ↔ θ)
4	3	anbi2i 482	. . 3 ⊢ ((φ ⋀ ψ) ↔ (φ ⋀ θ))
5		3imtr3g.3	. . 3 ⊢ (χ ↔ τ)
6	2, 4, 5	3imtr3 218	. 2 ⊢ ((φ ⋀ θ) → τ)
7	6	ex 373	1 ⊢ (φ → (θ → τ))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223

This theorem is referenced by:  3imtr4g 555  dvelimfALT 1155  dvelimf 1252  dvelimALT 1355  sspwb 2761  wetrep 2948  suceloni 3068  tfinds2 3171  imadif 3580  fiint 4572  fiintOLD 4573  aceq5lem5 4749  axpowndlem3 4963  lt2msq 5883  uzind 6207  infxpidmlem12 7564  subtop 7643  dscmet 7915  atabs2 10324

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain