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  1330  3orim123d  1331  hbbid  1589  spsbim  1857  moim  2109  moimv  2111  2euswapdc  2136  nelcon3d  2473  ralim  2556  ralimdaa  2563  ralimdv2  2567  rexim  2591  reximdv2  2596  rmoim  2965  ssel  3177  sstr2  3190  ssrexf  3245  ssrmof  3246  sscon  3297  ssdif  3298  unss1  3332  ssrin  3388  prel12  3801  uniss  3860  ssuni  3861  intss  3895  intssunim  3896  iunss1  3927  iinss1  3928  ss2iun  3931  disjss2  4013  disjss1  4016  ssbrd  4076  sspwb  4249  poss  4333  pofun  4347  soss  4349  sess1  4372  sess2  4373  ordwe  4612  wessep  4614  peano2  4631  finds  4636  finds2  4637  relss  4750  ssrel  4751  ssrel2  4753  ssrelrel  4763  xpsspw  4775  relop  4816  cnvss  4839  dmss  4865  dmcosseq  4937  funss  5277  imadif  5338  imain  5340  fss  5419  fun  5430  brprcneu  5551  isores3  5862  isopolem  5869  isosolem  5871  tposfn2  6324  tposfo2  6325  tposf1o2  6328  smores  6350  tfr1onlemaccex  6406  tfrcllemaccex  6419  iinerm  6666  xpdom2  6890  ssenen  6912  exmidpw  6969  exmidpweq  6970  nnnninfeq2  7195  recexprlemlol  7693  recexprlemupu  7695  axpre-ltwlin  7950  axpre-apti  7952  nnindnn  7960  nnind  9006  uzind  9437  hashfacen  10928  cau3lem  11279  tgcl  14300  epttop  14326  txcnp  14507  plycj  14997  gausslemma2dlem0i  15298  gausslemma2dlem1a  15299