Theorem 3imtr4g 198

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

Syntax hints:   → wi 4   ↔ wb 102

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

This theorem depends on definitions:  df-bi 114

This theorem is referenced by:  3anim123d  1225  3orim123d  1226  hbbid  1483  spsbim  1740  moim  1980  moimv  1982  2euswapdc  2007  ralim  2397  ralimdaa  2403  ralimdv2  2406  rexim  2430  reximdv2  2435  rmoim  2762  ssel  2966  sstr2  2979  sscon  3104  ssdif  3105  unss1  3139  ssrin  3189  prel12  3569  uniss  3628  ssuni  3629  intss  3663  intssunim  3664  iunss1  3695  iinss1  3696  ss2iun  3699  disjss2  3775  disjss1  3778  ssbrd  3832  sspwb  3979  poss  4062  pofun  4076  soss  4078  sess1  4101  sess2  4102  ordwe  4327  wessep  4329  peano2  4345  finds  4350  finds2  4351  relss  4454  ssrel  4455  ssrel2  4457  ssrelrel  4467  xpsspw  4477  relop  4513  cnvss  4535  dmss  4561  dmcosseq  4630  funss  4947  imadif  5006  imain  5008  fss  5081  fun  5090  brprcneu  5198  isores3  5482  isopolem  5488  isosolem  5490  tposfn2  5911  tposfo2  5912  tposf1o2  5915  smores  5937  iinerm  6208  xpdom2  6335  recexprlemlol  6781  recexprlemupu  6783  axpre-ltwlin  7014  axpre-apti  7016  nnindnn  7024  nnind  8005  uzind  8407  cau3lem  9933