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  1891  moim  2144  moimv  2146  2euswapdc  2171  nelcon3d  2509  ralim  2592  ralimdaa  2599  ralimdv2  2603  rexim  2627  reximdv2  2632  rmoim  3008  ssel  3222  sstr2  3235  ssrexf  3290  ssrmof  3291  sscon  3343  ssdif  3344  unss1  3378  ssrin  3434  prel12  3859  uniss  3919  ssuni  3920  intss  3954  intssunim  3955  iunss1  3986  iinss1  3987  ss2iun  3990  disjss2  4072  disjss1  4075  ssbrd  4136  sspwb  4314  poss  4401  pofun  4415  soss  4417  sess1  4440  sess2  4441  ordwe  4680  wessep  4682  peano2  4699  finds  4704  finds2  4705  relss  4819  ssrel  4820  ssrel2  4822  ssrelrel  4832  xpsspw  4844  relop  4886  cnvss  4909  dmss  4936  dmcosseq  5010  funss  5352  imadif  5417  imain  5419  fss  5501  fun  5516  brprcneu  5641  isores3  5966  isopolem  5973  isosolem  5975  tposfn2  6475  tposfo2  6476  tposf1o2  6479  smores  6501  tfr1onlemaccex  6557  tfrcllemaccex  6570  iinerm  6819  xpdom2  7058  ssenen  7080  exmidpw  7143  exmidpweq  7144  nnnninfeq2  7388  recexprlemlol  7906  recexprlemupu  7908  axpre-ltwlin  8163  axpre-apti  8165  nnindnn  8173  nnind  9218  uzind  9652  hashfacen  11163  pfxccatin12lem2  11378  cau3lem  11754  tgcl  14875  epttop  14901  txcnp  15082  plycj  15572  gausslemma2dlem0i  15876  gausslemma2dlem1a  15877  nnnninfex  16748