Theorem 3imtr4g 205

Description: More general version of 3imtr4i 201. 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	biimtrid 152	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	imbitrrdi 162	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3anim123d  1319  3orim123d  1320  hbbid  1575  spsbim  1843  moim  2090  moimv  2092  2euswapdc  2117  nelcon3d  2453  ralim  2536  ralimdaa  2543  ralimdv2  2547  rexim  2571  reximdv2  2576  rmoim  2939  ssel  3150  sstr2  3163  ssrexf  3218  ssrmof  3219  sscon  3270  ssdif  3271  unss1  3305  ssrin  3361  prel12  3772  uniss  3831  ssuni  3832  intss  3866  intssunim  3867  iunss1  3898  iinss1  3899  ss2iun  3902  disjss2  3984  disjss1  3987  ssbrd  4047  sspwb  4217  poss  4299  pofun  4313  soss  4315  sess1  4338  sess2  4339  ordwe  4576  wessep  4578  peano2  4595  finds  4600  finds2  4601  relss  4714  ssrel  4715  ssrel2  4717  ssrelrel  4727  xpsspw  4739  relop  4778  cnvss  4801  dmss  4827  dmcosseq  4899  funss  5236  imadif  5297  imain  5299  fss  5378  fun  5389  brprcneu  5509  isores3  5816  isopolem  5823  isosolem  5825  tposfn2  6267  tposfo2  6268  tposf1o2  6271  smores  6293  tfr1onlemaccex  6349  tfrcllemaccex  6362  iinerm  6607  xpdom2  6831  ssenen  6851  exmidpw  6908  exmidpweq  6909  nnnninfeq2  7127  recexprlemlol  7625  recexprlemupu  7627  axpre-ltwlin  7882  axpre-apti  7884  nnindnn  7892  nnind  8935  uzind  9364  hashfacen  10816  cau3lem  11123  tgcl  13567  epttop  13593  txcnp  13774