Theorem 3imtr4g 203

Description: More general version of 3imtr4i 199. 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 150	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	syl6ibr 160	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3anim123d  1250  3orim123d  1251  hbbid  1507  spsbim  1764  moim  2005  moimv  2007  2euswapdc  2032  ralim  2422  ralimdaa  2428  ralimdv2  2431  rexim  2455  reximdv2  2460  rmoim  2791  ssel  2993  sstr2  3006  sscon  3106  ssdif  3107  unss1  3141  ssrin  3191  prel12  3563  uniss  3622  ssuni  3623  intss  3657  intssunim  3658  iunss1  3689  iinss1  3690  ss2iun  3693  disjss2  3769  disjss1  3772  ssbrd  3826  sspwb  3971  poss  4053  pofun  4067  soss  4069  sess1  4092  sess2  4093  ordwe  4318  wessep  4320  peano2  4336  finds  4341  finds2  4342  relss  4445  ssrel  4446  ssrel2  4448  ssrelrel  4458  xpsspw  4468  relop  4504  cnvss  4526  dmss  4552  dmcosseq  4621  funss  4940  imadif  4999  imain  5001  fss  5074  fun  5083  brprcneu  5191  isores3  5475  isopolem  5481  isosolem  5483  tposfn2  5904  tposfo2  5905  tposf1o2  5908  smores  5930  iinerm  6201  xpdom2  6328  recexprlemlol  6816  recexprlemupu  6818  axpre-ltwlin  7049  axpre-apti  7051  nnindnn  7059  nnind  8055  uzind  8458  cau3lem  10000