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  1356  3orim123d  1357  hbbid  1624  spsbim  1892  moim  2145  moimv  2147  2euswapdc  2172  nelcon3d  2518  ralim  2601  ralimdaa  2608  ralimdv2  2612  rexim  2636  reximdv2  2641  rmoim  3018  ssel  3232  sstr2  3245  ssrexf  3300  ssrmof  3301  sscon  3353  ssdif  3354  unss1  3388  ssrin  3446  sspw  3682  prel12  3875  uniss  3935  ssuni  3936  intss  3970  intssunim  3971  iunss1  4002  iinss1  4003  ss2iun  4006  disjss2  4088  disjss1  4091  ssbrd  4152  sspwb  4332  poss  4419  pofun  4433  soss  4435  sess1  4458  sess2  4459  ordwe  4698  wessep  4700  peano2  4717  finds  4722  finds2  4723  relss  4837  ssrel  4838  ssrel2  4840  ssrelrel  4850  xpsspw  4862  relop  4905  cnvss  4928  dmss  4955  dmcosseq  5029  funss  5371  imadif  5436  imain  5438  fss  5521  fun  5536  brprcneu  5663  isores3  5988  isopolem  5995  isosolem  5997  tposfn2  6497  tposfo2  6498  tposf1o2  6501  smores  6523  tfr1onlemaccex  6579  tfrcllemaccex  6592  iinerm  6841  xpdom2  7082  ssenen  7105  exmidpw  7168  exmidpweq  7169  nnnninfeq2  7420  recexprlemlol  7941  recexprlemupu  7943  axpre-ltwlin  8198  axpre-apti  8200  nnindnn  8208  nnind  9253  uzind  9689  hashfacen  11208  pfxccatin12lem2  11423  cau3lem  11799  tgcl  14929  epttop  14955  txcnp  15136  plycj  15626  gausslemma2dlem0i  15930  gausslemma2dlem1a  15931  nnnninfex  16800