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  1586  spsbim  1854  moim  2102  moimv  2104  2euswapdc  2129  nelcon3d  2466  ralim  2549  ralimdaa  2556  ralimdv2  2560  rexim  2584  reximdv2  2589  rmoim  2953  ssel  3164  sstr2  3177  ssrexf  3232  ssrmof  3233  sscon  3284  ssdif  3285  unss1  3319  ssrin  3375  prel12  3786  uniss  3845  ssuni  3846  intss  3880  intssunim  3881  iunss1  3912  iinss1  3913  ss2iun  3916  disjss2  3998  disjss1  4001  ssbrd  4061  sspwb  4234  poss  4316  pofun  4330  soss  4332  sess1  4355  sess2  4356  ordwe  4593  wessep  4595  peano2  4612  finds  4617  finds2  4618  relss  4731  ssrel  4732  ssrel2  4734  ssrelrel  4744  xpsspw  4756  relop  4795  cnvss  4818  dmss  4844  dmcosseq  4916  funss  5254  imadif  5315  imain  5317  fss  5396  fun  5407  brprcneu  5527  isores3  5837  isopolem  5844  isosolem  5846  tposfn2  6292  tposfo2  6293  tposf1o2  6296  smores  6318  tfr1onlemaccex  6374  tfrcllemaccex  6387  iinerm  6634  xpdom2  6858  ssenen  6880  exmidpw  6937  exmidpweq  6938  nnnninfeq2  7158  recexprlemlol  7656  recexprlemupu  7658  axpre-ltwlin  7913  axpre-apti  7915  nnindnn  7923  nnind  8966  uzind  9395  hashfacen  10851  cau3lem  11158  tgcl  14041  epttop  14067  txcnp  14248