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  1319  3orim123d  1320  hbbid  1575  spsbim  1843  moim  2090  moimv  2092  2euswapdc  2117  nelcon3d  2453  ralim  2536  ralimdaa  2543  ralimdv2  2547  rexim  2571  reximdv2  2576  rmoim  2940  ssel  3151  sstr2  3164  ssrexf  3219  ssrmof  3220  sscon  3271  ssdif  3272  unss1  3306  ssrin  3362  prel12  3773  uniss  3832  ssuni  3833  intss  3867  intssunim  3868  iunss1  3899  iinss1  3900  ss2iun  3903  disjss2  3985  disjss1  3988  ssbrd  4048  sspwb  4218  poss  4300  pofun  4314  soss  4316  sess1  4339  sess2  4340  ordwe  4577  wessep  4579  peano2  4596  finds  4601  finds2  4602  relss  4715  ssrel  4716  ssrel2  4718  ssrelrel  4728  xpsspw  4740  relop  4779  cnvss  4802  dmss  4828  dmcosseq  4900  funss  5237  imadif  5298  imain  5300  fss  5379  fun  5390  brprcneu  5510  isores3  5818  isopolem  5825  isosolem  5827  tposfn2  6269  tposfo2  6270  tposf1o2  6273  smores  6295  tfr1onlemaccex  6351  tfrcllemaccex  6364  iinerm  6609  xpdom2  6833  ssenen  6853  exmidpw  6910  exmidpweq  6911  nnnninfeq2  7129  recexprlemlol  7627  recexprlemupu  7629  axpre-ltwlin  7884  axpre-apti  7886  nnindnn  7894  nnind  8937  uzind  9366  hashfacen  10818  cau3lem  11125  tgcl  13649  epttop  13675  txcnp  13856