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  5819  isopolem  5826  isosolem  5828  tposfn2  6270  tposfo2  6271  tposf1o2  6274  smores  6296  tfr1onlemaccex  6352  tfrcllemaccex  6365  iinerm  6610  xpdom2  6834  ssenen  6854  exmidpw  6911  exmidpweq  6912  nnnninfeq2  7130  recexprlemlol  7628  recexprlemupu  7630  axpre-ltwlin  7885  axpre-apti  7887  nnindnn  7895  nnind  8938  uzind  9367  hashfacen  10819  cau3lem  11126  tgcl  13704  epttop  13730  txcnp  13911