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  1353  3orim123d  1354  hbbid  1621  spsbim  1889  moim  2142  moimv  2144  2euswapdc  2169  nelcon3d  2506  ralim  2589  ralimdaa  2596  ralimdv2  2600  rexim  2624  reximdv2  2629  rmoim  3004  ssel  3218  sstr2  3231  ssrexf  3286  ssrmof  3287  sscon  3338  ssdif  3339  unss1  3373  ssrin  3429  prel12  3849  uniss  3909  ssuni  3910  intss  3944  intssunim  3945  iunss1  3976  iinss1  3977  ss2iun  3980  disjss2  4062  disjss1  4065  ssbrd  4126  sspwb  4302  poss  4389  pofun  4403  soss  4405  sess1  4428  sess2  4429  ordwe  4668  wessep  4670  peano2  4687  finds  4692  finds2  4693  relss  4806  ssrel  4807  ssrel2  4809  ssrelrel  4819  xpsspw  4831  relop  4872  cnvss  4895  dmss  4922  dmcosseq  4996  funss  5337  imadif  5401  imain  5403  fss  5485  fun  5499  brprcneu  5622  isores3  5945  isopolem  5952  isosolem  5954  tposfn2  6418  tposfo2  6419  tposf1o2  6422  smores  6444  tfr1onlemaccex  6500  tfrcllemaccex  6513  iinerm  6762  xpdom2  6998  ssenen  7020  exmidpw  7081  exmidpweq  7082  nnnninfeq2  7307  recexprlemlol  7824  recexprlemupu  7826  axpre-ltwlin  8081  axpre-apti  8083  nnindnn  8091  nnind  9137  uzind  9569  hashfacen  11071  pfxccatin12lem2  11279  cau3lem  11641  tgcl  14754  epttop  14780  txcnp  14961  plycj  15451  gausslemma2dlem0i  15752  gausslemma2dlem1a  15753  nnnninfex  16476