Theorem 3imtr4g 194

Description: More general version of 3imtr4i 190. 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 141	. 2 ⊢ (φ → (θ → χ))
4		3imtr4g.3	. 2 ⊢ (τ ↔ χ)
5	3, 4	syl6ibr 151	1 ⊢ (φ → (θ → τ))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3anim123d  1213  3orim123d  1214  hbbid  1464  spsbim  1721  moim  1961  moimv  1963  2euswapdc  1988  ralim  2374  ralimdaa  2380  ralimdv2  2383  rexim  2407  reximdv2  2412  rmoim  2734  ssel  2933  sstr2  2946  sscon  3071  ssdif  3072  unss1  3106  ssrin  3156  prel12  3533  uniss  3592  ssuni  3593  intss  3627  intssunim  3628  iunss1  3659  iinss1  3660  ss2iun  3663  disjss2  3739  disjss1  3742  ssbrd  3796  sspwb  3943  poss  4026  pofun  4040  soss  4042  sess1  4059  sess2  4060  peano2  4261  finds  4266  finds2  4267  relss  4370  ssrel  4371  ssrel2  4373  ssrelrel  4383  xpsspw  4393  relop  4429  cnvss  4451  dmss  4477  dmcosseq  4546  funss  4863  imadif  4922  imain  4924  fss  4997  fun  5006  brprcneu  5114  isores3  5398  isopolem  5404  isosolem  5406  tposfn2  5822  tposfo2  5823  tposf1o2  5826  smores  5848  iinerm  6114  xpdom2  6241  recexprlemlol  6596  recexprlemupu  6598  axpre-ltwlin  6727  axpre-apti  6729  nnind  7671  uzind  8085