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  2147  moimv  2149  2euswapdc  2174  nelcon3d  2520  ralim  2603  ralimdaa  2610  ralimdv2  2614  rexim  2638  reximdv2  2643  rmoim  3021  ssel  3236  sstr2  3249  ssrexf  3304  ssrmof  3305  sscon  3357  ssdif  3358  unss1  3392  ssrin  3450  sspw  3687  prel12  3880  uniss  3940  ssuni  3941  intss  3975  intssunim  3976  iunss1  4007  iinss1  4008  ss2iun  4011  disjss2  4093  disjss1  4096  ssbrd  4157  sspwb  4337  poss  4424  pofun  4438  soss  4440  sess1  4463  sess2  4464  ordwe  4703  wessep  4705  peano2  4722  finds  4727  finds2  4728  relss  4842  ssrel  4843  ssrel2  4845  ssrelrel  4855  xpsspw  4867  relop  4910  cnvss  4933  dmss  4960  dmcosseq  5034  funss  5376  imadif  5441  imain  5443  fss  5526  fun  5541  brprcneu  5668  isores3  5994  isopolem  6001  isosolem  6003  tposfn2  6510  tposfo2  6511  tposf1o2  6514  smores  6536  tfr1onlemaccex  6592  tfrcllemaccex  6605  iinerm  6854  xpdom2  7095  ssenen  7118  exmidpw  7181  exmidpweq  7182  nnnninfeq2  7433  recexprlemlol  7957  recexprlemupu  7959  axpre-ltwlin  8214  axpre-apti  8216  nnindnn  8224  nnind  9270  uzind  9707  hashfacen  11233  pfxccatin12lem2  11448  cau3lem  11824  tgcl  15055  epttop  15081  txcnp  15262  plycj  15752  gausslemma2dlem0i  16056  gausslemma2dlem1a  16057  nnnninfex  16926