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  1353  3orim123d  1354  hbbid  1621  spsbim  1889  moim  2142  moimv  2144  2euswapdc  2169  nelcon3d  2506  ralim  2589  ralimdaa  2596  ralimdv2  2600  rexim  2624  reximdv2  2629  rmoim  3005  ssel  3219  sstr2  3232  ssrexf  3287  ssrmof  3288  sscon  3339  ssdif  3340  unss1  3374  ssrin  3430  prel12  3850  uniss  3910  ssuni  3911  intss  3945  intssunim  3946  iunss1  3977  iinss1  3978  ss2iun  3981  disjss2  4063  disjss1  4066  ssbrd  4127  sspwb  4304  poss  4391  pofun  4405  soss  4407  sess1  4430  sess2  4431  ordwe  4670  wessep  4672  peano2  4689  finds  4694  finds2  4695  relss  4809  ssrel  4810  ssrel2  4812  ssrelrel  4822  xpsspw  4834  relop  4876  cnvss  4899  dmss  4926  dmcosseq  5000  funss  5341  imadif  5405  imain  5407  fss  5489  fun  5503  brprcneu  5626  isores3  5949  isopolem  5956  isosolem  5958  tposfn2  6425  tposfo2  6426  tposf1o2  6429  smores  6451  tfr1onlemaccex  6507  tfrcllemaccex  6520  iinerm  6769  xpdom2  7008  ssenen  7030  exmidpw  7091  exmidpweq  7092  nnnninfeq2  7317  recexprlemlol  7834  recexprlemupu  7836  axpre-ltwlin  8091  axpre-apti  8093  nnindnn  8101  nnind  9147  uzind  9579  hashfacen  11087  pfxccatin12lem2  11299  cau3lem  11662  tgcl  14775  epttop  14801  txcnp  14982  plycj  15472  gausslemma2dlem0i  15773  gausslemma2dlem1a  15774  nnnninfex  16534