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  1332  3orim123d  1333  hbbid  1599  spsbim  1867  moim  2119  moimv  2121  2euswapdc  2146  nelcon3d  2483  ralim  2566  ralimdaa  2573  ralimdv2  2577  rexim  2601  reximdv2  2606  rmoim  2978  ssel  3191  sstr2  3204  ssrexf  3259  ssrmof  3260  sscon  3311  ssdif  3312  unss1  3346  ssrin  3402  prel12  3818  uniss  3877  ssuni  3878  intss  3912  intssunim  3913  iunss1  3944  iinss1  3945  ss2iun  3948  disjss2  4030  disjss1  4033  ssbrd  4094  sspwb  4268  poss  4353  pofun  4367  soss  4369  sess1  4392  sess2  4393  ordwe  4632  wessep  4634  peano2  4651  finds  4656  finds2  4657  relss  4770  ssrel  4771  ssrel2  4773  ssrelrel  4783  xpsspw  4795  relop  4836  cnvss  4859  dmss  4886  dmcosseq  4959  funss  5299  imadif  5363  imain  5365  fss  5447  fun  5459  brprcneu  5582  isores3  5897  isopolem  5904  isosolem  5906  tposfn2  6365  tposfo2  6366  tposf1o2  6369  smores  6391  tfr1onlemaccex  6447  tfrcllemaccex  6460  iinerm  6707  xpdom2  6941  ssenen  6963  exmidpw  7020  exmidpweq  7021  nnnninfeq2  7246  recexprlemlol  7759  recexprlemupu  7761  axpre-ltwlin  8016  axpre-apti  8018  nnindnn  8026  nnind  9072  uzind  9504  hashfacen  11003  cau3lem  11500  tgcl  14611  epttop  14637  txcnp  14818  plycj  15308  gausslemma2dlem0i  15609  gausslemma2dlem1a  15610  nnnninfex  16100