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  4174  sspwb  4358  poss  4445  pofun  4459  soss  4461  sess1  4484  sess2  4485  ordwe  4725  wessep  4727  peano2  4744  finds  4749  finds2  4750  relss  4864  ssrel  4865  ssrel2  4867  ssrelrel  4877  xpsspw  4889  relop  4932  cnvss  4955  dmss  4982  dmcosseq  5056  funss  5399  imadif  5464  imain  5466  fss  5549  fun  5564  brprcneu  5691  isores3  6024  isopolem  6031  isosolem  6033  tposfn2  6542  tposfo2  6543  tposf1o2  6546  smores  6568  tfr1onlemaccex  6624  tfrcllemaccex  6637  iinerm  6886  xpdom2  7135  ssenen  7158  exmidpw  7221  exmidpweq  7222  nnnninfeq2  7475  recexprlemlol  7999  recexprlemupu  8001  axpre-ltwlin  8256  axpre-apti  8258  nnindnn  8266  nnind  9329  uzind  9767  hashfacen  11305  pfxccatin12lem2  11524  cau3lem  11902  tgcl  15307  epttop  15333  txcnp  15514  plycj  16004  gausslemma2dlem0i  16398  gausslemma2dlem1a  16399  nnnninfex  17288