Theorem 3imtr4g 204

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3anim123d  1262  3orim123d  1263  hbbid  1519  spsbim  1778  moim  2019  moimv  2021  2euswapdc  2046  nelcon3d  2368  ralim  2445  ralimdaa  2452  ralimdv2  2455  rexim  2479  reximdv2  2484  rmoim  2830  ssel  3033  sstr2  3046  sscon  3149  ssdif  3150  unss1  3184  ssrin  3240  prel12  3637  uniss  3696  ssuni  3697  intss  3731  intssunim  3732  iunss1  3763  iinss1  3764  ss2iun  3767  disjss2  3847  disjss1  3850  ssbrd  3908  sspwb  4067  poss  4149  pofun  4163  soss  4165  sess1  4188  sess2  4189  ordwe  4419  wessep  4421  peano2  4438  finds  4443  finds2  4444  relss  4554  ssrel  4555  ssrel2  4557  ssrelrel  4567  xpsspw  4579  relop  4617  cnvss  4640  dmss  4666  dmcosseq  4736  funss  5068  imadif  5128  imain  5130  fss  5207  fun  5218  brprcneu  5333  isores3  5632  isopolem  5639  isosolem  5641  tposfn2  6069  tposfo2  6070  tposf1o2  6073  smores  6095  tfr1onlemaccex  6151  tfrcllemaccex  6164  iinerm  6404  xpdom2  6627  ssenen  6647  exmidpw  6704  recexprlemlol  7282  recexprlemupu  7284  axpre-ltwlin  7515  axpre-apti  7517  nnindnn  7525  nnind  8536  uzind  8956  hashfacen  10372  cau3lem  10678  tgcl  11932  epttop  11958