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  1314  3orim123d  1315  hbbid  1568  spsbim  1836  moim  2083  moimv  2085  2euswapdc  2110  nelcon3d  2446  ralim  2529  ralimdaa  2536  ralimdv2  2540  rexim  2564  reximdv2  2569  rmoim  2931  ssel  3141  sstr2  3154  ssrexf  3209  ssrmof  3210  sscon  3261  ssdif  3262  unss1  3296  ssrin  3352  prel12  3756  uniss  3815  ssuni  3816  intss  3850  intssunim  3851  iunss1  3882  iinss1  3883  ss2iun  3886  disjss2  3967  disjss1  3970  ssbrd  4030  sspwb  4199  poss  4281  pofun  4295  soss  4297  sess1  4320  sess2  4321  ordwe  4558  wessep  4560  peano2  4577  finds  4582  finds2  4583  relss  4696  ssrel  4697  ssrel2  4699  ssrelrel  4709  xpsspw  4721  relop  4759  cnvss  4782  dmss  4808  dmcosseq  4880  funss  5215  imadif  5276  imain  5278  fss  5357  fun  5368  brprcneu  5487  isores3  5791  isopolem  5798  isosolem  5800  tposfn2  6242  tposfo2  6243  tposf1o2  6246  smores  6268  tfr1onlemaccex  6324  tfrcllemaccex  6337  iinerm  6581  xpdom2  6805  ssenen  6825  exmidpw  6882  exmidpweq  6883  nnnninfeq2  7101  recexprlemlol  7575  recexprlemupu  7577  axpre-ltwlin  7832  axpre-apti  7834  nnindnn  7842  nnind  8881  uzind  9310  hashfacen  10758  cau3lem  11065  tgcl  12779  epttop  12805  txcnp  12986