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 ⊢ (𝜑 → (𝜃 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3anim123d  1360  3orim123d  1361  hbbid  1628  spsbim  1896  moim  2151  moimv  2153  2euswapdc  2178  nelcon3d  2526  ralim  2609  ralimdaa  2616  ralimdv2  2620  rexim  2644  reximdv2  2649  rmoim  3027  ssel  3242  sstr2  3255  ssrexf  3310  ssrmof  3311  sscon  3363  ssdif  3364  unss1  3398  ssrin  3456  sspw  3702  prel12  3896  uniss  3956  ssuni  3957  intss  3991  intssunim  3992  iunss1  4023  iinss1  4024  ss2iun  4027  disjss2  4109  disjss1  4112  ssbrd  4173  sspwb  4356  poss  4443  pofun  4457  soss  4459  sess1  4482  sess2  4483  ordwe  4723  wessep  4725  peano2  4742  finds  4747  finds2  4748  relss  4862  ssrel  4863  ssrel2  4865  ssrelrel  4875  xpsspw  4887  relop  4930  cnvss  4953  dmss  4980  dmcosseq  5054  funss  5396  imadif  5461  imain  5463  fss  5546  fun  5561  brprcneu  5688  isores3  6021  isopolem  6028  isosolem  6030  tposfn2  6537  tposfo2  6538  tposf1o2  6541  smores  6563  tfr1onlemaccex  6619  tfrcllemaccex  6632  iinerm  6881  xpdom2  7129  ssenen  7152  exmidpw  7215  exmidpweq  7216  nnnninfeq2  7469  recexprlemlol  7993  recexprlemupu  7995  axpre-ltwlin  8250  axpre-apti  8252  nnindnn  8260  nnind  9320  uzind  9757  hashfacen  11284  pfxccatin12lem2  11503  cau3lem  11880  tgcl  15165  epttop  15191  txcnp  15372  plycj  15862  gausslemma2dlem0i  16176  gausslemma2dlem1a  16177  nnnninfex  17065