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	|- ( ph -> ( ps -> ch ) )
3imtr4g.2	|- ( th <-> ps )
3imtr4g.3	|- ( ta <-> ch )

Assertion

Ref	Expression
3imtr4g	|- ( ph -> ( th -> ta ) )

Proof of Theorem 3imtr4g

Step	Hyp	Ref	Expression
1		3imtr4g.2	. . 3 |- ( th <-> ps )
2		3imtr4g.1	. . 3 |- ( ph -> ( ps -> ch ) )
3	1, 2	biimtrid 152	. 2 |- ( ph -> ( th -> ch ) )
4		3imtr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	imbitrrdi 162	1 |- ( ph -> ( th -> ta ) )

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  3178  sstr2  3191  ssrexf  3246  ssrmof  3247  sscon  3298  ssdif  3299  unss1  3333  ssrin  3389  prel12  3802  uniss  3861  ssuni  3862  intss  3896  intssunim  3897  iunss1  3928  iinss1  3929  ss2iun  3932  disjss2  4014  disjss1  4017  ssbrd  4077  sspwb  4250  poss  4334  pofun  4348  soss  4350  sess1  4373  sess2  4374  ordwe  4613  wessep  4615  peano2  4632  finds  4637  finds2  4638  relss  4751  ssrel  4752  ssrel2  4754  ssrelrel  4764  xpsspw  4776  relop  4817  cnvss  4840  dmss  4866  dmcosseq  4938  funss  5278  imadif  5339  imain  5341  fss  5422  fun  5433  brprcneu  5554  isores3  5865  isopolem  5872  isosolem  5874  tposfn2  6333  tposfo2  6334  tposf1o2  6337  smores  6359  tfr1onlemaccex  6415  tfrcllemaccex  6428  iinerm  6675  xpdom2  6899  ssenen  6921  exmidpw  6978  exmidpweq  6979  nnnninfeq2  7204  recexprlemlol  7710  recexprlemupu  7712  axpre-ltwlin  7967  axpre-apti  7969  nnindnn  7977  nnind  9023  uzind  9454  hashfacen  10945  cau3lem  11296  tgcl  14384  epttop  14410  txcnp  14591  plycj  15081  gausslemma2dlem0i  15382  gausslemma2dlem1a  15383