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  1194  3orim123d  1195  hbbid  1440  spsbim  1697  moim  1937  moimv  1939  2euswapdc  1964  ralim  2349  ralimdaa  2355  ralimdv2  2358  rexim  2382  reximdv2  2387  rmoim  2708  ssel  2907  sstr2  2920  sscon  3045  ssdif  3046  unss1  3080  ssrin  3130  prel12  3505  uniss  3564  ssuni  3565  intss  3599  intssunim  3600  iunss1  3631  iinss1  3632  ss2iun  3635  disjss2  3711  disjss1  3714  ssbrd  3768  sspwb  3915  poss  3998  pofun  4012  soss  4014  sess1  4031  sess2  4032  peano2  4233  finds  4238  finds2  4239  relss  4342  ssrel  4343  ssrel2  4345  ssrelrel  4355  xpsspw  4365  relop  4401  cnvss  4423  dmss  4449  dmcosseq  4518  funss  4834  imadif  4893  imain  4895  fss  4968  fun  4976  brprcneu  5084  isores3  5368  isopolem  5374  isosolem  5376  tposfn2  5791  tposfo2  5792  tposf1o2  5795  smores  5817  iinerm  6077  recexprlemlol  6447  recexprlemupu  6449  axpre-ltwlin  6572  axpre-apti  6574  nnind  7513  uzind  7913