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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3anim123d  1309  3orim123d  1310  hbbid  1563  spsbim  1831  moim  2078  moimv  2080  2euswapdc  2105  nelcon3d  2442  ralim  2525  ralimdaa  2532  ralimdv2  2536  rexim  2560  reximdv2  2565  rmoim  2927  ssel  3136  sstr2  3149  ssrexf  3204  ssrmof  3205  sscon  3256  ssdif  3257  unss1  3291  ssrin  3347  prel12  3751  uniss  3810  ssuni  3811  intss  3845  intssunim  3846  iunss1  3877  iinss1  3878  ss2iun  3881  disjss2  3962  disjss1  3965  ssbrd  4025  sspwb  4194  poss  4276  pofun  4290  soss  4292  sess1  4315  sess2  4316  ordwe  4553  wessep  4555  peano2  4572  finds  4577  finds2  4578  relss  4691  ssrel  4692  ssrel2  4694  ssrelrel  4704  xpsspw  4716  relop  4754  cnvss  4777  dmss  4803  dmcosseq  4875  funss  5207  imadif  5268  imain  5270  fss  5349  fun  5360  brprcneu  5479  isores3  5783  isopolem  5790  isosolem  5792  tposfn2  6234  tposfo2  6235  tposf1o2  6238  smores  6260  tfr1onlemaccex  6316  tfrcllemaccex  6329  iinerm  6573  xpdom2  6797  ssenen  6817  exmidpw  6874  exmidpweq  6875  nnnninfeq2  7093  recexprlemlol  7567  recexprlemupu  7569  axpre-ltwlin  7824  axpre-apti  7826  nnindnn  7834  nnind  8873  uzind  9302  hashfacen  10749  cau3lem  11056  tgcl  12704  epttop  12730  txcnp  12911