Theorem 3imtr4g 204

Description: More general version of 3imtr4i 200. 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	syl5bi 151	. 2 |- ( ph -> ( th -> ch ) )
4		3imtr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	syl6ibr 161	1 |- ( ph -> ( th -> ta ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3anim123d  1280  3orim123d  1281  hbbid  1537  spsbim  1797  moim  2039  moimv  2041  2euswapdc  2066  nelcon3d  2388  ralim  2465  ralimdaa  2472  ralimdv2  2476  rexim  2500  reximdv2  2505  rmoim  2854  ssel  3057  sstr2  3070  ssrexf  3125  ssrmof  3126  sscon  3176  ssdif  3177  unss1  3211  ssrin  3267  prel12  3664  uniss  3723  ssuni  3724  intss  3758  intssunim  3759  iunss1  3790  iinss1  3791  ss2iun  3794  disjss2  3875  disjss1  3878  ssbrd  3936  sspwb  4098  poss  4180  pofun  4194  soss  4196  sess1  4219  sess2  4220  ordwe  4450  wessep  4452  peano2  4469  finds  4474  finds2  4475  relss  4586  ssrel  4587  ssrel2  4589  ssrelrel  4599  xpsspw  4611  relop  4649  cnvss  4672  dmss  4698  dmcosseq  4768  funss  5100  imadif  5161  imain  5163  fss  5242  fun  5253  brprcneu  5368  isores3  5670  isopolem  5677  isosolem  5679  tposfn2  6117  tposfo2  6118  tposf1o2  6121  smores  6143  tfr1onlemaccex  6199  tfrcllemaccex  6212  iinerm  6455  xpdom2  6678  ssenen  6698  exmidpw  6755  recexprlemlol  7382  recexprlemupu  7384  axpre-ltwlin  7618  axpre-apti  7620  nnindnn  7628  nnind  8646  uzind  9066  hashfacen  10472  cau3lem  10778  tgcl  12076  epttop  12102  txcnp  12282