Theorem 3imtr4g 261

Description: More general version of 3imtr4i 257. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)

Hypotheses

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

Assertion

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

Proof of Theorem 3imtr4g

Step	Hyp	Ref	Expression
1		3imtr4g.2	. . 3 ⊢ (θ ↔ ψ)
2		3imtr4g.1	. . 3 ⊢ (φ → (ψ → χ))
3	1, 2	syl5bi 208	. 2 ⊢ (φ → (θ → χ))
4		3imtr4g.3	. 2 ⊢ (τ ↔ χ)
5	3, 4	syl6ibr 218	1 ⊢ (φ → (θ → τ))

Syntax hints:   → wi 4   ↔ wb 176

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 177

This theorem is referenced by:  3anim123d  1259  3orim123d  1260  moim  2250  morimv  2252  2euswap  2280  ralim  2685  ralimdaa  2691  ralimdv2  2694  rexim  2718  reximdv2  2723  moeq3  3013  rmoim  3035  2reuswap  3038  ssel  3267  sstr2  3279  sscon  3400  ssdif  3401  unss1  3432  ssrin  3480  difin0ss  3616  r19.2z  3639  uniss  3912  ssuni  3913  intss  3947  intssuni  3948  iunss1  3980  iinss1  3981  ss2iun  3984  sspwb  4118  findsd  4410  ncfinlower  4483  evenoddnnnul  4514  spfinsfincl  4539  vfinspss  4551  vfinspclt  4552  vinf  4555  ssbrd  4680  ssrel  4844  cnvss  4885  dmss  4906  dmcosseq  4973  funss  5126  fss  5230  fun  5236  eqfnfv  5392  clos1conn  5879  clos1is  5881  enadjlem1  6059  enprmaplem6  6081  leltctr  6212  nnltp1c  6262  nncdiv3  6277  spacind  6287  nchoicelem17  6305